Cyclic proofs of program termination in separation logic
Article
Brotherston, J., Bornat, R. and Calcagno, C. 2008. Cyclic proofs of program termination in separation logic. ACM SIGPLAN Notices. 43 (1), pp. 101-112. https://doi.org/10.1145/1328897.1328453
Type | Article |
---|---|
Title | Cyclic proofs of program termination in separation logic |
Authors | Brotherston, J., Bornat, R. and Calcagno, C. |
Abstract | We propose a novel approach to proving the termination of heap-manipulating 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. |
Research Group | Foundations of Computing group |
Publisher | Association for Computing Machinery (ACM) |
Journal | ACM SIGPLAN Notices |
ISSN | 0362-1340 |
Publication process dates | |
Deposited | 03 Jul 2013 |
Output status | Published |
Digital Object Identifier (DOI) | https://doi.org/10.1145/1328897.1328453 |
Language | English |
https://repository.mdx.ac.uk/item/8429x
27
total views0
total downloads5
views this month0
downloads this month