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.

Josh Berdine is an associate researcher working in the Programming Principles and Tools group at Microsoft Research, Cambridge. His research pursuits revolve around automatically verifying and analyzing pointer programs. Primarily memory safety, data structure integrity, and termination properties are considered, on one hand using a lightweight fragment of separation logic (O'Hearn and Reynolds', among others, Hoare-style logic, tailored to modular reasoning about pointers), and on the other hand using separation logic inspired type theory. He previously worked in Peter O'Hearn's group at Queen Mary, University of London, and for John Reynolds at Carnegie Mellon University.