Automated analysis of programs is one of the major success stories in PL. The goal here is to algorithmically infer properties of a program’s runtime behavior without executing the program on concrete inputs. This may be done for many reasons, including optimization and reasoning about correctness. If you are trying to optimize a program, it helps to know that a statement executed within a loop always performs the same update, and can therefore be moved out of the loop. If you want to be certain that your C program doesn’t have buffer overflows, you want to infer bounds on the indices used for array accesses in the program.
Over the years, systems for program analysis have increased in sophistication and entered the mainstream of software development. But how do you know that what your analysis tells you is correct? To be certain that it is, we must relate the program’s semantics – what the program does at runtime – to what the analysis algorithm computes. The framework of abstract interpretation is the gold standard for doing so.
Radhia Cousot, co-inventor of abstract interpretation, passed away earlier this summer after a long struggle with cancer. While her death was tragic, I am consoled that she lived to see her work impact the world in a way that most researchers can only dream of.