Estonian Winter Schools in Computer Science
Eesti arvutiteaduse talvekoolid
Département d'Informatique (DI)
École Normale Supérieure (ENS), France
The objective of the course is to present the formal bases of Abstract Interpretation theory in simple terms and to discuss various applications in Computer Science.
Lesson 1: Motivations for formal methods;
On formal methods and computer-aided verification;
Motivations for Abstract Interpretation;
Informal introduction to Abstract Interpretation (using a graphical language);
Basic elements of the theory of abstract interpretation: Galois connections, function abstraction, fixpoints, fixpoint approximation and exact abstraction, soundness, completeness.
Lesson 2: Elements of Abstract Interpretation (cont'd):
Moore families, closure operators, complements on Galois connections, abstract domains, combination of abtract domains, iterative fixpoint approximation with convergence acceleration by widening/narrowing, completion of abstract domains, the lattice of Abstract Interpretations;
An introductory application to the constructive design of algorithms for grammar analysis;
Application to program verification by predicate abstraction.
Lesson 3: Application of Abstract Interpretation to static program analysis;
Formal design of an abstract interpretor.
The following two introductory papers are recommended as a written pedagogical support for this course:
The last lesson is based on the following paper:
Modified Monday, Oct 12, 2015 at 17:19 EEST+0300 by firstname.lastname@example.org