An SMT-based verification framework for software systems handling arrays
Staff - Faculty of Informatics
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 ∃*∀*-first-order formulae. We further show that the theoretical importance of this result has a practical relevance: Once the (problematic) nested quantifiers are suitable handled, acceleration offers a precise (not over-approximated) alternative to abstraction solutions.
Third, we present new decision procedures for quantified fragments of the theories of arrays. Our decision procedures are fully declarative, parametric in the theories describing the structure of the indexes and the elements of the arrays and orthogonal with respect to known results.
Forth, by leveraging our new results on acceleration and decision procedures, we show that the problem of checking the safety of an important class of programs with arrays is fully decidable.
The thesis presents along with theoretical results practical engineering strategies for the effective implementation of a framework combining the aforementioned results: The declarative nature of our contributions allows for the definition of an integrated framework able to effectively check the safety of programs handling array variables while overcoming the individual limitations of the presented techniques.
- Prof. Natasha Sharygina, Università della Svizzera italiana, Switzerland (Research Advisor)
- Prof. Rolf Krause, Università della Svizzera italiana, Switzerland (Internal Member)
- Prof. Nate Nystrom, Università della Svizzera italiana, Switzerland (Internal Member)
- Prof. Viktor Kuncak, EPFL, Switzerland (External Member)
- Prof. Nikolaj Bjorner, Microsoft Research Redmond, USA (External Member)