Name
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.
|
Year | DOI | Venue |
|---|---|---|
2007 | 10.1007/978-3-540-69738-1_5 | VMCAI |
Keywords | Field | DocType |
container data structure,finite map,hash table,complex dynamically instantiable data,data structure operation,data structure invariants,individual data structure,first-order theorem provers,jahob data structure verification,appropriate hash table bucket,shape analysis,complex dynamics,data structure,first order logic,theorem prover,first order,interactive theorem proving,higher order logic | Data structure,Programming language,Linked list,Computer science,sort,Correctness,Automated theorem proving,Theoretical computer science,Binary search tree,Hash table,Proof assistant | Conference |
Volume | ISSN | Citations |
4349 | 0302-9743 | 23 |
PageRank | References | Authors |
1.00 | 25 | 5 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Charles Bouillaguet | 1 | 212 | 13.32 |
| Viktor Kuncak | 2 | 1129 | 70.57 |
| Thomas Wies | 3 | 515 | 28.26 |
| Karen Zee | 4 | 183 | 8.50 |
| Martin C. Rinard | 5 | 4739 | 277.55 |