Introduction to abstract interpretation

Ing. Giuseppe Lettieri
Dipartimento di Ingegneria dell'Informazione: Elettronica, Informatica, Telecomunicazioni, Università di Pisa

12 hours, 3 credits

September 14 - September 16, 2009

Dipartimento di Ingegneria dell'Informazione: Elettronica, Informatica, Telecomunicazioni, Largo Lucio Lazzarino (formerly via Diotisalvi), meeting room

Abstract

Abstract interpretation is a theory of approximation of mathematical structures, in particular those involved in the semantic models of computer systems. Abstract interpretation theory underlies many static program analyses, as implemented in compilers or dedicated tools, and can be used to build new analyses systematically and prove them correct. The aim of this series of lessons is to introduce the main ideas of abstract interpretation, with reference to both its mathematical foundations and its practical applications, such as Java bytecode verification.

Syllabus

Mathematical foundations

Partially ordered sets, lattices

CPOs and fixpoints

Abstract interpretation

Galois connections, closure operators, Moore families

Approximation through widening/narrowing

Examples

Constant propagation

Java bytecode verification