Francesco Ranzato & Roberto Giacobazzi

History of Abstract Interpretation

We trace the roots of Abstract Interpretation and its role as a fundamental theoretical framework to understand and design program analysis and program verification methods.

Starting from the historical roots of program verification and formal methods, form A.M. Turing to C.A.R. Hoare, we show how abstract interpretation fits this mainstream in perfect continuity and how this theory shaped the literature and the practice in program analysis in the last 40 years, providing powerful tools for designing static program analyzers, automatic verifiers of software/hardware systems, type systems, security protocol analyzers, and algorithms for formal languages.

The top 5 most cited articles at ACM POPL include three articles on abstract interpretation, in particular the most cited article, which according to Google scholar has more than 7000 citations. We then will trace the beginning of its industrialization form the very first systematic use in verification of embedded systems to the nowadays wide spread use in high-end static program analysers.

Noteworthy examples include: (1) the Polyspace static analyzer for C/C++ and Ada programs has been fully conceived and designed by abstract interpretation and is successfully commercialized by TheMathWorks (2) Astree is a C static analyzer based on abstract interpretation, conceived and designed by Patrick and Radhia Cousot’s research group at ENS Paris, marketed by AbsInt GmbH (Germany), and used in the defense/aerospace (Airbus, Honda), electronic (Siemens), and automotive industries (Daimler); (3) Infer is a static analysis tool for detecting memory and concurrency bugs in Java/C/C++/Objective-C code, developed by Facebook, based on abstract interpretation and routinely used by Facebook software engineers.

We will survey the birth and evolution of abstract interpretation starting from the celebrated Cousot-Cousot's POPL77 paper and landing, through a 40+ years journey, to the current state-of-the-art of this research discipline. We will also give some personal hints on the main future challenges faced by abstract interpretation research.