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 rogram'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

• Type: Conference
• Year: 2006
• Where: CAV
• Authors: Josh Berdine, Byron Cook, Dino Distefano, Peter W. O'Hearn
• Keywords: Abstract Interpretation, CAV 2006, Hardware, Implies Termination, Program Termination Analysis