Proving Termination by Divergence

2007_SEFM_BCHR screenshot

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

Domagoj Babic, Byron Cook, Alan J. Hu., Zvonimir Rakamaric
Proving Termination by Divergence
Proceedings of the 5th IEEE International Conference on Software Engineering and Formal Methods (SEFM 2007), 93--102, 2007.

BibTeX

@inproceedings{2007_SEFM_BCHR,
  title = {Proving Termination by Divergence},
  author = {Domagoj Babic and Byron Cook and Alan J. Hu. and Zvonimir Rakamaric},
  booktitle = {Proceedings of the 5th IEEE International Conference on Software Engineering and Formal Methods (SEFM 2007)},
  editor = {Kedar S. Namjoshi and Tomohiro Yoneda},
  publisher = {IEEE Computer Society},
  pages = {93--102},
  year = {2007}
}