Using first-order theorem provers in the Jahob data structure verification system
Bouillaguet C, Kuncak V, Wies T, Zee K, Rinard M. 2007. Using first-order theorem provers in the Jahob data structure verification system. 8th International Conference on Verification, Model Checking, and Abstract Interpretation. VMCAI: Verification, Model Checking and Abstract Interpretation, LNCS, vol. 4349, 74–88.
Download
No fulltext has been uploaded. References only!
Conference Paper
| Published
| English
Scopus indexed
Author
Bouillaguet, Charles;
Kuncak, Viktor;
Wies, ThomasISTA;
Zee, Karen;
Rinard, Martin
Series Title
LNCS
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 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 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.
Publishing Year
Date Published
2007-01-01
Proceedings Title
8th International Conference on Verification, Model Checking, and Abstract Interpretation
Publisher
Springer
Volume
4349
Page
74 - 88
Conference
VMCAI: Verification, Model Checking and Abstract Interpretation
Conference Location
Nice, France
Conference Date
2007-01-14 – 2007-01-16
IST-REx-ID
Cite this
Bouillaguet C, Kuncak V, Wies T, Zee K, Rinard M. Using first-order theorem provers in the Jahob data structure verification system. In: 8th International Conference on Verification, Model Checking, and Abstract Interpretation. Vol 4349. Springer; 2007:74-88. doi:10.1007/978-3-540-69738-1_5
Bouillaguet, C., Kuncak, V., Wies, T., Zee, K., & Rinard, M. (2007). Using first-order theorem provers in the Jahob data structure verification system. In 8th International Conference on Verification, Model Checking, and Abstract Interpretation (Vol. 4349, pp. 74–88). Nice, France: Springer. https://doi.org/10.1007/978-3-540-69738-1_5
Bouillaguet, Charles, Viktor Kuncak, Thomas Wies, Karen Zee, and Martin Rinard. “Using First-Order Theorem Provers in the Jahob Data Structure Verification System.” In 8th International Conference on Verification, Model Checking, and Abstract Interpretation, 4349:74–88. Springer, 2007. https://doi.org/10.1007/978-3-540-69738-1_5.
C. Bouillaguet, V. Kuncak, T. Wies, K. Zee, and M. Rinard, “Using first-order theorem provers in the Jahob data structure verification system,” in 8th International Conference on Verification, Model Checking, and Abstract Interpretation, Nice, France, 2007, vol. 4349, pp. 74–88.
Bouillaguet C, Kuncak V, Wies T, Zee K, Rinard M. 2007. Using first-order theorem provers in the Jahob data structure verification system. 8th International Conference on Verification, Model Checking, and Abstract Interpretation. VMCAI: Verification, Model Checking and Abstract Interpretation, LNCS, vol. 4349, 74–88.
Bouillaguet, Charles, et al. “Using First-Order Theorem Provers in the Jahob Data Structure Verification System.” 8th International Conference on Verification, Model Checking, and Abstract Interpretation, vol. 4349, Springer, 2007, pp. 74–88, doi:10.1007/978-3-540-69738-1_5.