eprintid: 1455002
rev_number: 60
eprint_status: archive
userid: 608
dir: disk0/01/45/50/02
datestamp: 2014-11-12 11:26:39
lastmod: 2021-09-25 23:36:26
status_changed: 2014-11-12 11:26:39
type: proceedings_section
metadata_visibility: show
item_issues_count: 0
creators_name: Brotherston, J
creators_name: Fuhs, C
creators_name: Pérez, JAN
creators_name: Gorogiannis, N
title: A decision procedure for satisfiability in separation logic with inductive predicates
ispublished: pub
divisions: UCL
divisions: B04
divisions: C05
divisions: F48
note: 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).
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.
date: 2014-08
publisher: Association for Computing Machinery (ACM)
official_url: http://dx.doi.org/10.1145/2603088.2603091
vfaculties: VENG
oa_status: green
full_text_type: pub
language: eng
primo: open
primo_central: open_green
verified: verified_manual
elements_source: Scopus
elements_id: 992406
doi: 10.1145/2603088.2603091
isbn_13: 9781450328869
lyricists_name: Brotherston, James
lyricists_name: Fuhs, Carsten
lyricists_name: Navarro Perez, Juan
lyricists_id: JBROT05
lyricists_id: CFUHS19
lyricists_id: JANAV96
full_text_status: public
place_of_pub: New York, US
event_title: 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 
book_title: 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
citation:        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   
 
document_url: https://discovery.ucl.ac.uk/id/eprint/1455002/2/a25-brotherston.pdf