Abstraction and Approximation via Abstract Interpretation:
a systematic approach to (declarative) program analysis and verification

Giorgio Levi
Dipartimento di Informatica, Università di Pisa
levi@di.unipi.it                          http://www.di.unipi.it/~levi.html

Course summary

1. overview

2. the basic theory of abstract interpretation
3. an abstract interpreter for functional programs
4. systematic derivation of a type inference algorithm for untyped l-calculus
5. properties of the type abstract interpreter
6. abstract interpretation for comparative semantics of logic programs
        6.1. foundations and semantics
        6.2. the lattice of observables
        6.3 finite failure and infinite computations
7. abstract interpretation for the analysis of logic programs
        7.1. groundness analysis
        7.2. termination and other analyses
8. abstract interpretation for the verification of logic programs
         8.1. (abstract) diagnosis
         8.2. verification
         8.3. verification wrt finite failure and termination
9. how to transform an analyzer into a verifier
          9.1. type verification in functional programming
          9.2. types in logic programs: part 1 and part 2
          9.3. combining inference and verification
10. domain refinement operators