Sciweavers

POPL
2008
ACM
14 years 11 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. Judgement...
James Brotherston, Richard Bornat, Cristiano Calca...