Abstract
Automated software verification has made great progress recently, and a key enabler of this progress has been the advances in efficient, automated decision procedures suitable for verification (Boolean satisfiability solvers and satisfiability-modulo-theories (SMT) solvers). Verifying general software, however, requires reasoning about unbounded, linked, heap-allocated data structures, which in turn motivates the need for a logical theory for such structures that includes unbounded reachability. So far, none of the available SMT solvers supports such a theory. In this paper, we present our integration of a decision procedure that supports unbounded heap reachability into an available SMT solver. Using the extended SMT solver, we can efficiently verify examples of heap-manipulating programs that we could not verify before.
Citation
Zvonimir Rakamaric,
Roberto Bruttomesso,
Alan J. Hu.,
Alessandro Cimatti
Verifying Heap-Manipulating Programs in an SMT Framework
Proceedings of the 5th International Symposium on Automated Technology for Verification and Analysis (ATVA), 4762: 237--252, doi:10.1007/978-3-540-75596-8_18, 2007.
BibTeX
@inproceedings{2007_atva_rbhc,
title = {Verifying Heap-Manipulating Programs in an SMT Framework},
author = {Zvonimir Rakamaric and Roberto Bruttomesso and Alan J. Hu. and Alessandro Cimatti},
booktitle = {Proceedings of the 5th International Symposium on Automated Technology for Verification and Analysis (ATVA)},
series = {Lecture Notes in Computer Science},
volume = {4762},
publisher = {Springer},
editor = {Kedar S. Namjoshi and Tomohiro Yoneda},
pages = {237--252},
doi = {10.1007/978-3-540-75596-8_18},
year = {2007}
}
Acknowledgements
Supported by (1) a research grant from the Natural Sciences and Engineering Research Council of Canada, (2) a University of British Columbia Graduate Fellowship, (3) ORCHID, a project sponsored by Provincia Autonoma di Trento, and (4) a research grant from Intel.