Using First-Order Theorem Provers in Data Structure Verification System
Speaker: Charles Bouillaguet , Ecole Normale Superieure, Cachan, France
Date: August 29 2006
Time: 4:00PM to 5:00PM
Location: 32-D463 Star
Host: Martin Rinard & Viktor Kuncak, CSAIL
Contact: Mary McDavitt, 617-253-9620, mmcdavit@csail.mit.edu
ABSTRACT:
One of the main challenges in the verification of software
systems is the analysis of unbounded data structures with
dynamic memory allocation, such as linked data structures and
hash tables. Jahob is a data structure
verification system that generates a formula whose
validity implies the correctness of the program with
respect to its specification, as well as the absence of
run-time errors. Jahob discharges proof obligations using
several decision procedures. Current decision procedures
in Jahob target particular data structure properties such
as reachability and reasoning about sets with cardinality
constraints. However, many proof obligations that arise
in practice fall outside of this class, yet have
relatively short proofs. Resolution-based first-order
theorem provers are becoming increasingly effective at
proving formulas with short proofs. This talk shows how
we incorporated such theorem provers into our software
verification system and present the techniques that we
found necessary to make this integration feasible.
Our input formulas are written in a typed language that
contains a sort of objects and a disjoint sort of
integers. We show that, somewhat surprisingly, omitting
sort information (i) is both sound and complete, even in
the presence of a generic equality operator, and (ii)
makes theorem provers more effective at these formulas.
We have found that the effectiveness of theorem provers
dramatically decreases as the number of assumptions
increases. We describe simple heuristics for filtering
assumptions from first-order formulas that reduces input
problem size and speeds up the theorem proving process.
The combination of these techniques allowed us to verify
complex correctness properties of Java programs such as a
finite map implementated using functional ordered trees, a
mutable set implemented as an imperative linked list, a
hash table, and a simple library system that uses these
container data structures. For example, our
implementation of a functional ordered tree spans a few
hundred lines of code; our system takes one minute to
verify that the operations correctly update the finite map
and preserve the ordering of elements in the tree.
See other events that are part of
See other events happening in August 2006
