Abstract
Abstract interpretation is a very general formalism introduced by Patrick Cousot and Radhia Cousot in 1977 to describe and implement static analyses that are more precise than those achievable by data flow analysis. Beyond optimizations in compilers, abstract interpretation has enabled the realization of verification tools automatically showing the absence of runtime errors in large programs.
Abstract interpretation is traditionally formalized by two functions, an abstraction function α and a concretization function γ, which form a Galois correspondence between an abstract domain corresponding to the results of static analysis and the sets of concrete states corresponding to program executions. Elegantly, these two functions make it possible to " calculate " the abstract operators that implement static analysis, i.e. to systematically derive definitions of these operators that are correct and relatively complete by construction.
However, this classical presentation is problematic in the context of mechanization in Coq or other type-theoretic logic : the abstraction functions α are generally non-computable, and sometimes ill-defined. The fifth lecture developed an alternative presentation of abstract domains that doesn't use abstraction functions α, but only concretization predicates γ linking abstract objects and concrete states in a way that is fully definable in type theory. Abstract operators are no longer " computed " but given a priori and then verified a posteriori.
We followed this approach to build, in Coq, a generic static analyzer (a " abstract interpreter ") for IMP, and a very simple abstract domain for constant analysis. We then enhanced the accuracy of our analyzer with two techniques typical of abstract interpretation : the " backwards " analysis of Boolean expressions in conditionals and loops, and the computation of fixed points by iteration with enlargement. This has enabled us to obtain a fairly precise analysis of the variation intervals of variables in an IMP program.
