Using first-order theorem provers in the jahob data structure verification system

Charles Bouillaguet, Viktor Kuncak, Thomas Wies, Karen Zee, Martin Rinard

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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, 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 resolutionbased 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 often 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.

Original languageEnglish (US)
Title of host publicationVerification, Model Checking, and Abstract Interpretation, - 8th International Conference, VMCAI 2007, Proceedings
Pages74-88
Number of pages15
Volume4349 LNCS
StatePublished - 2007
Event8th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2007 - Nice, France
Duration: Jan 14 2007Jan 16 2007

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume4349 LNCS
ISSN (Print)03029743
ISSN (Electronic)16113349

Other

Other8th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2007
CountryFrance
CityNice
Period1/14/071/16/07

Fingerprint

Data structures
Data Structures
First-order
Theorem
Libraries
Verify
Correctness
Table
Ordered Trees
Theorem proving
Higher-order Logic
Theorem Proving
Search Trees
Experimental Results
First-order Logic
Container
Sort
Java
Containers
Null

ASJC Scopus subject areas

  • Computer Science(all)
  • Biochemistry, Genetics and Molecular Biology(all)
  • Theoretical Computer Science

Cite this

Bouillaguet, C., Kuncak, V., Wies, T., Zee, K., & Rinard, M. (2007). Using first-order theorem provers in the jahob data structure verification system. In Verification, Model Checking, and Abstract Interpretation, - 8th International Conference, VMCAI 2007, Proceedings (Vol. 4349 LNCS, pp. 74-88). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4349 LNCS).

Using first-order theorem provers in the jahob data structure verification system. / Bouillaguet, Charles; Kuncak, Viktor; Wies, Thomas; Zee, Karen; Rinard, Martin.

Verification, Model Checking, and Abstract Interpretation, - 8th International Conference, VMCAI 2007, Proceedings. Vol. 4349 LNCS 2007. p. 74-88 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4349 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Bouillaguet, C, Kuncak, V, Wies, T, Zee, K & Rinard, M 2007, Using first-order theorem provers in the jahob data structure verification system. in Verification, Model Checking, and Abstract Interpretation, - 8th International Conference, VMCAI 2007, Proceedings. vol. 4349 LNCS, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 4349 LNCS, pp. 74-88, 8th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2007, Nice, France, 1/14/07.
Bouillaguet C, Kuncak V, Wies T, Zee K, Rinard M. Using first-order theorem provers in the jahob data structure verification system. In Verification, Model Checking, and Abstract Interpretation, - 8th International Conference, VMCAI 2007, Proceedings. Vol. 4349 LNCS. 2007. p. 74-88. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
Bouillaguet, Charles ; Kuncak, Viktor ; Wies, Thomas ; Zee, Karen ; Rinard, Martin. / Using first-order theorem provers in the jahob data structure verification system. Verification, Model Checking, and Abstract Interpretation, - 8th International Conference, VMCAI 2007, Proceedings. Vol. 4349 LNCS 2007. pp. 74-88 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{03c2ae2519fa4b7a8677a20325fab86f,
title = "Using first-order theorem provers in the jahob data structure verification system",
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, 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 resolutionbased 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 often 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.",
author = "Charles Bouillaguet and Viktor Kuncak and Thomas Wies and Karen Zee and Martin Rinard",
year = "2007",
language = "English (US)",
isbn = "3540697357",
volume = "4349 LNCS",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "74--88",
booktitle = "Verification, Model Checking, and Abstract Interpretation, - 8th International Conference, VMCAI 2007, Proceedings",

}

TY - GEN

T1 - Using first-order theorem provers in the jahob data structure verification system

AU - Bouillaguet, Charles

AU - Kuncak, Viktor

AU - Wies, Thomas

AU - Zee, Karen

AU - Rinard, Martin

PY - 2007

Y1 - 2007

N2 - 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, 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 resolutionbased 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 often 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.

AB - 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, 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 resolutionbased 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 often 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.

UR - http://www.scopus.com/inward/record.url?scp=34547203542&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=34547203542&partnerID=8YFLogxK

M3 - Conference contribution

AN - SCOPUS:34547203542

SN - 3540697357

SN - 9783540697350

VL - 4349 LNCS

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 74

EP - 88

BT - Verification, Model Checking, and Abstract Interpretation, - 8th International Conference, VMCAI 2007, Proceedings

ER -