Automatic Termination Proofs for Programs with Shape-Shifting Heaps

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.

mutant.pdf
PDF file

In  Computer Aided Verification, 18th International Conference, CAV 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings

Publisher  Springer

Details

TypeInproceedings
Pages386-400
Volume4144
SeriesLecture Notes in Computer Science
ISBN3-540-37406-X
> Publications > Automatic Termination Proofs for Programs with Shape-Shifting Heaps