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