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

A decision procedure for satisfiability in separation logic with inductive predicates

Brotherston, J; Fuhs, C; Pérez, JAN; Gorogiannis, N; (2014) A decision procedure for satisfiability in separation logic with inductive predicates. In: Proceedings of the Joint Meeting of the 23rd EACSL Annual Conference on Computer Science Logic, CSL 2014 and the 29th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2014. Association for Computing Machinery (ACM): New York, US. Green open access

[thumbnail of a25-brotherston.pdf] PDF
a25-brotherston.pdf

Download (390kB)

Abstract

We show that the satisfiability problem for the "symbolic heap" fragment of separation logic with general inductively defined predicates- which includes most fragments employed in program verification - is decidable. Our decision procedure is based on the computation of a certain fixed point from the definition of an inductive predicate, called its "base", that exactly characterises its satisfiability. A complexity analysis of our decision procedure shows that it runs, in the worst case, in exponential time. In fact, we show that the satisfiability problem for our inductive predicates is EXPTIME- complete, and becomes NP-complete when the maximum arity over all predicates is bounded by a constant. Finally, we provide an implementation of our decision procedure, and analyse its performance both on a synthetically generated set of test formulas, and on a second test set harvested from the separation logic literature. For the large majority of these test cases, our tool reports times in the low milliseconds. Copyright © 2014 ACM.

Type: Proceedings paper
Title: A decision procedure for satisfiability in separation logic with inductive predicates
Event: 23rd EACSL Annual Conference on Computer Science Logic, CSL 2014 and the 29th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2014, Vienna, Austria — July 14 - 18, 2014
ISBN-13: 9781450328869
Open access status: An open access version is available from UCL Discovery
DOI: 10.1145/2603088.2603091
Publisher version: http://dx.doi.org/10.1145/2603088.2603091
Language: English
Additional information: Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for third-party components of this work must be honored. For all other uses, contact the owner/author(s) Copyright is held by the owner/author(s).
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/1455002
Downloads since deposit
128Downloads
Download activity - last month
Download activity - last 12 months
Downloads by country - last 12 months

Archive Staff Only

View Item View Item