Automatic termination proofs for programs with shape-shifting heaps. Draft available from http://www.research.microsoft.com/terminator/mutant_draft.pdf

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 interpreta-tion based on separation logic formulæ which tracks the depths of pieces of heaps. Finally, we combine these two techniques to produce an au-tomatic 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.