Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Automatic Termination Proofs for Programs with Shape-Shifting Heaps

Josh Berdine, Byron Cook, Dino Distefano, and Peter W. O'Hearn

Abstract

We describe a new program termination analysis designed to handle imperative programs whose termination depends on the mutation of the program's heap. We first describe how an abstract interpretation can be used to construct a finite number of relations which, if each is well-founded, implies termination. We then give an abstract interpretation based on separation logic formulae which tracks the depths of pieces of heaps. Finally, we combine these two techniques to produce an automatic termination prover. We show that the analysis is able to prove the termination of loops extracted from Windows device drivers that could not be proved terminating before by other means; we also discuss a previously unknown bug found with the analysis.

Details

Publication typeInproceedings
Published inComputer Aided Verification, 18th International Conference, CAV 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings
Pages386-400
Volume4144
SeriesLecture Notes in Computer Science
ISBN3-540-37406-X
PublisherSpringer
> Publications > Automatic Termination Proofs for Programs with Shape-Shifting Heaps