Abstract Interpretation

Semantics: We define the structural rule-based and then fixpoint prefix trace semantics of a simple subset of C. We define properties, in particular program properties and collecting semantics.

Abstraction: We formalize the abstraction and approximation of program properties and how a structural rule-based/fixpoint abstract semantics can be derived from the collecting semantics by calculational design.

Proofs: we show that verification methods and program logics are (non-computable) abstractions of the program collecting semantics.

Numerical abstractions: we introduce a few classical effectively computable abstractions of numerical properties of programs and discuss industrial static analysis applications.

Symbolic abstractions: we introduce a few abstractions of symbolic properties of programs and discuss opened problems. We conclude by a list of formal methods that can be formalized as abstract interpretations.