Static Analysis and Verification

This is an internal course for post-grads at ITI. If you want to attend as well, please email Jan Obdržálek.

Overview papers

Michael I. Schwartzbach: Lecture Notes on Static Analysis

Lecture notes from BRICS course on static analysis.

Abstract: These notes present principles and applications of static analysis of programs. We cover type analysis, lattice theory, control flow graphs, dataflow analysis, fixed-point algorithms, narrowing and widening, interprocedural analysis, control flow analysis, and pointer analysis. A tiny imperative programming language with heap pointers and function pointers is subjected to numerous different static analyses illustrating the techniques that are presented.

The style of presentation is intended to be precise but not overly formal. The readers are assumed to be familiar with advanced programming language concepts and the basics of compiler construction.

Abstract interpretation

P. Cousot, R. Cousot: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints

4th ACM SIGPLAN-SIGACT, 1977

Abstract: A program denotes computations in some universe of objects. Abstract interpretation of programs consists in using that denotation to describe computations in another universe of abstract objects, so that the results of abstract execution give some information on the actual computations. An intuitive example (which we borrow from Sintzoff [72]) is the rule of signs. The text -1515 * 17 may be understood to denote computations on the abstract universe {(+), (-), (±)} where the semantics of arithmetic operators is defined by the rule of signs. The abstract execution -1515 * 17 → -(+) * (+) → (-) * (+) → (-), proves that -1515 * 17 is a negative number. Abstract interpretation is concerned by a particular underlying structure of the usual universe of computations (the sign, in our example). It gives a summary of some facets of the actual executions of a program. In general this summary is simple to obtain but inaccurate (e.g. -1515 + 17 → -(+) + (+) → (-) + (+) → (±)). Despite its fundamentally incomplete results abstract interpretation allows the programmer or the compiler to answer questions which do not need full knowledge of program executions or which tolerate an imprecise answer, (e.g. partial correctness proofs of programs ignoring the termination problems, type checking, program optimizations which are not carried in the absence of certainty about their feasibility, …).

Comments: The original paper on abstract interpretation, a must read for everybody.

T. Ball, A. Podelski and S. Rajamani: Boolean and Cartesian Abstraction for Model Checking C Programs

TACAS 2001

Abstract: We show how to attack the problem of model checking a C program with recursive procedures using an abstraction that we formally define as the composition of the Boolean and the Cartesian abstractions. It is implemented through a source-to-source transformation into a ‘Boolean’ C program; we give an algorithm to compute the transformation with a cost that is exponential in its theoretical worst-case complexity but feasible in practice.

Comments: Presents the abstraction used in Microsoft's SLAM project. A nice concrete example how the general Cousot&Cousot style abstraction is used.

Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar and Gregoire Sutre: Lazy Abstraction

POPL 2002

Abstract: One approach to model checking software is based on the abstract-check-refine paradigm: build an abstract model, then check the desired property, and if the check fails, refine the model and start over. We introduce the concept of lazy abstraction to integrate and optimize the three phases of the abstract-check-refine loop. Lazy abstraction continuously builds and refines a single abstract model on demand, driven by the model checker, so that different parts of the model may exhibit different degrees of precision, namely just enough to verify the desired property. We present an algorithm for model checking safety properties using lazy abstraction and describe an implementation of the algorithm applied to C programs. We also provide sufficient conditions for the termination of the method.

Comments: Presents the lazy abstraction used in the BLAST project.

Tool presentations I

SLAM/SDV (Microsoft)

SLAM project homepage

BLAST (originally Berkeley)

BLAST project homepage
Dirk Beyer, Thomas A. Henzinger, Ranjit Jhala, and Rupak Majumdar:The Software Model Checker Blast: Applications to Software Engineering. STTT 2007, based on FASE 2005.


Jan Obdržálek

Last modified: Friday, 17-Oct-2008 08:29:30 CEST

Valid XHTML 1.0 StrictValid CSS!