[ list |
abstracts |
bib |
http ]

## On Using First-Order Theorem Provers in a the Jahob Data Structure Verification System

paper pdf
paper ps
### Abstract

This paper presents our integration of efficient
resolution-based theorem provers into the Jahob data
structure verification system. Our experimental results
show that this approach enables Jahob to automatically
verify the correctness of a range of complex dynamically
instantiable data structures, including data structures
such as hash tables and search trees, without the need for
interactive theorem proving or techniques tailored to
individual data structures.
Our primary technical results include: (1) a translation
from higher-order logic to first-order logic that enables
the application of resolution-based theorem provers and
(2) a proof that eliminating type (sort) information in
formulas is both sound and complete, even in the presence
of a generic equality operator. Our
experimental results show that the elimination of
type information dramatically decreases the time required
to prove the resulting formulas.
These techniques enabled us to verify complex correctness
properties of Java programs such as a mutable set
implemented as an imperative linked list, a finite map
implemented as a functional ordered tree, a hash table
with a mutable array, and a simple library system example
that uses these container data structures. Our system
verifies (in a matter of minutes) that data structure
operations correctly update the finite map, that they
preserve data structure invariants (such as ordering of
elements, membership in appropriate hash table buckets, or
relationships between sets and relations), and that there
are no run-time errors such as null dereferences or array
out of bounds accesses.

### Citation

Charles Bouillaguet, Viktor Kuncak, Thomas Wies, Karen Zee, and Martin Rinard.
On using first-order theorem provers in a the Jahob data structure
verification system.
Technical Report MIT-CSAIL-TR-2006-072, MIT, November 2006.
Full version of
[55].### BibTex Entry

@TECHREPORT{BouillaguetETAL06UsingFirstOrderTheoremProvers,
author = {Charles Bouillaguet and Viktor Kuncak and Thomas Wies and Karen Zee and Martin Rinard},
title = {On Using First-Order Theorem Provers in a the {J}ahob Data Structure Verification System},
institution = {MIT},
number = {MIT-CSAIL-TR-2006-072},
year = 2006,
url = {http://hdl.handle.net/1721.1/34874},
month = {November},
note = {Full version of \cite{BouillaguetETAL07UsingFirstOrderTheoremProvers}},
localurl = {http://lara.epfl.ch/~kuncak/papers/BouillaguetETAL06UsingFirstOrderTheoremProvers.pdf}
}

[ list |
abstracts |
bib |
http ]