zbMATH — the first resource for mathematics

Automatic termination proofs for programs with shape-shifting heaps. (English) Zbl 1188.68109
Ball, Thomas (ed.) et al., Computer aided verification. 18th international conference, CAV 2006, Seattle, WA, USA, August 17–20, 2006. Proceedings. Berlin: Springer (ISBN 3-540-37406-X/pbk). Lecture Notes in Computer Science 4144, 386-400 (2006).
Summary: 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 formulæ 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.
For the entire collection see [Zbl 1114.68002].

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
Full Text: DOI