UCL Discovery
UCL home » Library Services » Electronic resources » UCL Discovery

Disproving Inductive Entailments in Separation Logic via Base Pair Approximation

Brotherston, J; Gorogiannis, N; (2015) Disproving Inductive Entailments in Separation Logic via Base Pair Approximation. In: Automated Reasoning with Analytic Tableaux and Related Methods: 24th International Conference, TABLEAUX 2015, Wroclaw, Poland, September 21-24, 2015, Proceedings. (pp. pp. 287-303). Springer International Publishing: Switzerland. Green open access

[thumbnail of final.pdf]
Preview
Text
final.pdf - Accepted Version

Download (198kB) | Preview

Abstract

We give a procedure for establishing the invalidity of logical entailments in the symbolic heap fragment of separation logic with user-defined inductive predicates, as used in program verification. This disproof procedure attempts to infer the existence of a countermodel to an entailment by comparing computable model summaries, a.k.a. bases (modified from earlier work), of its antecedent and consequent. Our method is sound and terminating, but necessarily incomplete. Experiments with the implementation of our disproof procedure indicate that it can correctly identify a substantial proportion of the invalid entailments that arise in practice, at reasonably low time cost. Accordingly, it can be used, e.g., to improve the output of theorem provers by returning “no” answers in addition to “yes” and “unknown” answers to entailment questions, and to speed up proof search or automated theory exploration by filtering out invalid entailments.

Type: Proceedings paper
Title: Disproving Inductive Entailments in Separation Logic via Base Pair Approximation
Event: 24th International Conference, TABLEAUX 2015
ISBN-13: 9783319243115
Open access status: An open access version is available from UCL Discovery
DOI: 10.1007/978-3-319-24312-2_20
Publisher version: http://dx.doi.org/10.1007/978-3-319-24312-2_20
Language: English
Additional information: Copyright © Springer International Publishing Switzerland 2015. The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-319-24312-2_20
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/1474215
Downloads since deposit
89Downloads
Download activity - last month
Download activity - last 12 months
Downloads by country - last 12 months

Archive Staff Only

View Item View Item