PRINCIPLES OF ABSTRACT INTERPRETATION

Modern societies are increasingly dependent upon the proper functioning of computer systems. Yet, computer programs are riddled with flaws that at best are inconvenient and annoying, and at worst, have extremely damaging consequences.
Formal methods aim at using the rigor of mathematics for the specification, development, and verification of reliable and robust software and hardware systems. The ultimate objective of formal methods is to verify the correctness of computer systems and to have this verification completely automated, using computers. This objective is hard to achieve because of undecidability: no computer can correctly answer with finite time and memory resources every question relative to the correctness of an arbitrary computer system.
Therefore all automated formal methods that provide answers in finite time on undecidable questions have to make compromises to escape this inevitable limitation of the power of computer systems:

Deductive methods based on automated theorem proving requires human guidance and assistance, which may be an overwhelming task;
Model-checking can only enumerate the behaviours of finite systems, and small enough to avoid time and memory explosion;
Static program analysis may be unsound or correct but not be precise enough to answer the desired questions.

The principles of abstract interpretation establish the foundations of all formal methods, their design, (un)soundness and (in)completeness, relative to the semantics of a programming language. The course formalizes exact and approximate semantic property abstraction with three main applications:

Semantics of programming languages (formally defining the possible executions of a program);
Design of deductive methods by abstract interpretation;
Design of static analysis by abstract interpretation.

The course has 5 days each with 4 academic hours (of 45 minutes). Electronic slides as well as notes will be provided. The notes include the mathematical prerequisites and contain additional material for further study.

The final exam will consist in a seminar presenting a scientific paper about the application of the abstract interpretation theory to some contexts. A list of possible papers will be published in this webpage during the course.

Inglese