Seminars at the Faculty of Informatics

An SMT-based verification framework for software systems handling arrays

You are cordially invited to attend the PhD Dissertation Defense of Francesco ALBERTI on Tuesday, February 17th at 10h30 in room 003 (Informatics building)

Recent advantages in the areas of automated reasoning and first-order theorem proving paved the way to the developing of effective tools for the rigorous formal analysis of computer systems. Nowadays many formal verification frameworks are built over highly engineered tools (SMT-solvers) implementing decision procedures for quantifier-free fragments of theories of interest for (dis)proving properties of software or hardware products.

The goal of this thesis is go beyond the quantifier-free case and enable sound and effective solutions for the analysis of software systems requiring the usage of quantifiers. This is the case, for example, of software systems handling array variables, since meaningful properties about arrays, e.g., "the array is sorted", can be expressed only by exploiting quantification.

The first contribution of this thesis is the definition of a new Lazy Abstraction with Interpolants framework in which arrays can be handled in a natural manner. We identify a fragment of the theory of arrays admitting quantifier-free interpolation and provide an effective quantifier-free interpolation algorithm. The combination of this result with an important preprocessing technique allows the generation of the required quantified formulae.

Second, we prove that accelerations (i.e. transitive closures) of an interesting class of relations over arrays are definable in the theory of arrays via *