Unfortunately, the problem of determining whether a program is correct is undecidable. Program-analysis and verification tools sidestep the tar-pit of undecidability by working on an abstraction of a program, which over-approximates the behavior of the original program. The theory underlying this approach is called abstract interpretation. Abstract interpretation provides a way to obtain information about the possible states that a program reaches during execution, but without actually running the program on specific inputs. Instead, it explores the program’s behavior for all possible inputs, thereby accounting for all possible states that the program can reach. Operationally, one can think of abstract interpretation as running the program “in the aggregate.” That is, rather than executing the program on ordinary states, the program is executed on abstract states, which are finite-sized descriptors that represent collections of states.

However, there is a glitch: abstract interpretation has a well-deserved reputation of being a kind of “black art,” and consequently difficult to work with. This talk will describe a twenty-year quest address this issue by raising the level of automation in abstract interpretation. I will present several different approaches to creating correct-by-construction analyzers. Somewhat surprisingly, this research has recently allowed us to establish connections between our problem and several other areas of computer science, including machine learning, knowledge compilation, data integration, and constraint programming.

Thomas Reps is the J. Barkley Rosser Professor of Computer Science and holds the Rajiv and Ritu Batra Chair at the University of Wisconsin. He has worked on many aspects of automated program analysis and is co-founder and president of GrammaTech, a leading developer of software-assurance and software security tools.