Automatic cyclic termination proofs for recursive procedures in separation logic

Rowe, Reuben and Brotherston, James (2017) Automatic cyclic termination proofs for recursive procedures in separation logic. In: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs - CPP 2017. ACM pp. 53-65. ISBN 978-1-4503-4705-1. (doi:https://doi.org/10.1145/3018610.3018623) (Full text available)

PDF - Author's Accepted Manuscript

Creative Commons Licence
This work is licensed under a Creative Commons Attribution 4.0 International License.
Download (301kB) Preview
[img]
Preview
Official URL
https://doi.org/10.1145/3018610.3018623

Abstract

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 pre- and 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.

Item Type: Conference or workshop item (Proceeding)
Divisions: Faculties > Sciences > School of Computing
Faculties > Sciences > School of Computing > Programming Languages and Systems Group
Depositing User: Reuben Rowe
Date Deposited: 24 Nov 2017 13:30 UTC
Last Modified: 27 Nov 2017 16:35 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/64716 (The current URI for this page, for reference purposes)
Rowe, Reuben: https://orcid.org/0000-0002-4271-9078
  • Depositors only (login required):

Downloads

Downloads per month over past year