Rowe, RNS;
Brotherston, J;
(2017)
Automatic cyclic termination proofs for recursive procedures in separation logic.
In:
CPP 2017 Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs.
(pp. pp. 53-65).
Association for Computing Machinery: New York.
Preview |
Text
p53-rowe.pdf - Published Version Download (603kB) | Preview |
Abstract
© 2017 ACM.We describe a formal verification framework and tool implementation, based upon cyclic proofs, for certifying the safe termination of imperative pointer programs with recursive procedures. Our assertions are symbolic heaps in separation logic with user defined inductive predicates; we employ explicit approximations of these predicates as our termination measures. This enables us to extend cyclic proof to programs with procedures by relating these measures across the preand postconditions of procedure calls. We provide an implementation of our formal proof system in the CYCLIST theorem proving framework, and evaluate its performance on a range of examples drawn from the literature on program termination. Our implementation extends the current state-of-the-art in cyclic proof-based program verification, enabling automatic termination proofs of a larger set of programs than previously possible.
| Type: | Proceedings paper |
|---|---|
| Title: | Automatic cyclic termination proofs for recursive procedures in separation logic |
| Event: | 6th ACM SIGPLAN Conference on Certified Programs and Proofs |
| ISBN-13: | 9781450347051 |
| Open access status: | An open access version is available from UCL Discovery |
| DOI: | 10.1145/3018610.3018623 |
| Language: | English |
| Additional information: | This work is licensed under a Creative Commons Attribution International 4.0 Licence. |
| Keywords: | Automated proof search, Cyclic proof, Explicit approximation, Imperative programming, Proof Certificates, Separation logic, Termination |
| UCL classification: | UCL UCL > Provost and Vice Provost Offices > UCL BEAMS UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science |
| URI: | https://discovery.ucl.ac.uk/id/eprint/1546183 |
Loading...
Loading...Loading...Loading...Archive Staff Only
 |
View Item |
