Sciweavers

Share
POPL
2008
ACM

Cyclic proofs of program termination in separation logic

9 years 2 months ago
Cyclic proofs of program termination in separation logic
We propose a novel approach to proving the termination of heapmanipulating programs, which combines separation logic with cyclic proof within a Hoare-style proof system. Judgements in this system express (guaranteed) termination of the program when started from a given line in the program and in a state satisfying a given precondition, which is expressed as a formula of separation logic. The proof rules of our system are of two types: logical rules that operate on preconditions; and symbolic execution rules that capture the effect of executing program commands. Our logical preconditions employ inductively defined predicates to describe heap properties, and proofs in our system are cyclic proofs: cyclic derivations in which some inductive predicate is unfolded infinitely often along every infinite path, thus allowing us to discard all infinite paths in the proof by an infinite descent argument. Moreover, the use of this soundness condition enables us to avoid the explicit construction ...
James Brotherston, Richard Bornat, Cristiano Calca
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2008
Where POPL
Authors James Brotherston, Richard Bornat, Cristiano Calcagno
Comments (0)
books