Lecture 08: Convergence of Abstract Interpretation. Predicate Abstraction
Idea of abstract interpretation: overapproximate computation in the lattice of sets of states
Abstract Interpretation Recipe
Mapping Fixpoints under Lattice Morphisms
Comparing Fixpoints of Sequences
Chaotic Iteration in Abstract Interpretation
Termination of Abstract Interpretation
Widening in Variable Range Analysis
Continued in Lecture 09
References
- Lecture notes on static analysis by Michael Schwartzbach (sections 4,5,6,7 in particular), and pdf file
- Tiger book, chapters 10, 17
- Abstract Interpretation in a Nutshell by Patrick Cousot (also a course at MIT)
Scala sources illustrating basic concepts of Abstract Interpretation:
- DiGraphs.scala - graphs
- SimpleCFG.scala - simple control-flow graphs
- SimpleAST.scala - simple abstract syntax tre
- SimpleTranslate.scala - translation from AST to CFG
- Lattices.scala - lattices with some examples, and definition of product
- DataFlowAnalysis.scala - simplest fixpoint iteration algorithm parameterized by transfer functions i.e. by sp#
- ConcreteAnalysis.scala - transfer functions for Collecting Semantics
- SignAnalysis.scala - transfer functions for sign analysis