A decision procedure for satisfiability in separation logic with inductive predicates

Conference paper


Brotherston, J., Fuhs, C., Pérez, J. and Gorogiannis, N. 2014. A decision procedure for satisfiability in separation logic with inductive predicates. CSL-LICS 2014. Vienna, Austria 14 - 18 Jul 2014 Association for computing machinery. pp. 1-10 https://doi.org/10.1145/2603088.2603091
TypeConference paper
TitleA decision procedure for satisfiability in separation logic with inductive predicates
AuthorsBrotherston, J., Fuhs, C., Pérez, J. and Gorogiannis, N.
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.

Research GroupFoundations of Computing group
ConferenceCSL-LICS 2014
Page range1-10
ISBN
Hardcover9781450328869
PublisherAssociation for computing machinery
Publication dates
Print14 Jul 2014
Publication process dates
Deposited12 May 2015
Output statusPublished
Copyright Statement

Copyright © 2014 Owner/Author

Digital Object Identifier (DOI)https://doi.org/10.1145/2603088.2603091
LanguageEnglish
Book titleProceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) - CSL-LICS '14
Permalink -

https://repository.mdx.ac.uk/item/854xq

Restricted files

Accepted author manuscript

  • 14
    total views
  • 1
    total downloads
  • 0
    views this month
  • 0
    downloads this month

Export as