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
Accepted author manuscript
File Access Level
Open
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

Log in to edit
File access - Request a copy

Restricted files

Accepted author manuscript

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

Export as

Related outputs

A true positives theorem for a static race detector
Gorogiannis, N., O'Hearn, P. and Sergey, I. 2019. A true positives theorem for a static race detector. POPL 2019. Cascais, Portugal 12 - 19 Jan 2019 Association for Computing Machinery (ACM). pp. 1-29 https://doi.org/10.1145/3290370
RacerD: compositional static race detection
Blackshear, S., Gorogiannis, N., O'Hearn, P. and Sergey, I. 2018. RacerD: compositional static race detection. Association for Computing Machinery (ACM). https://doi.org/10.1145/3276514
Analysis and verification of ECA rules in intelligent environments
Cacciagrano, D., Corradini, F., Culmone, R., Gorogiannis, N., Mostarda, L., Raimondi, F. and Vannucchi, C. 2018. Analysis and verification of ECA rules in intelligent environments. Journal of Ambient Intelligence and Smart Environments. 10 (3), pp. 261-273. https://doi.org/10.3233/AIS-180487
MIRTO: an open-source robotic platform for education
Androutsopoulos, K., Aristodemou, L., Boender, J., Bottone, M., Currie, E., El-Aroussi, I., Fields, B., Gheri, L., Gorogiannis, N., Heeney, M., Micheletti, M., Loomes, M., Margolis, M., Petridis, M., Piermarteri, A., Primiero, G., Raimondi, F. and Weldin, N. 2018. MIRTO: an open-source robotic platform for education. 3rd European Conference on Software Engineering Education. Seeon, Germany 14 - 15 Jun 2018 Association for Computing Machinery (ACM). pp. 55-62 https://doi.org/10.1145/3209087.3209106
Biabduction (and related problems) in array separation logic
Brotherston, J., Gorogiannis, N. and Kanovich, M. 2017. Biabduction (and related problems) in array separation logic. International Conference on Automated Deduction. Gothenburg 08 - 11 Aug 2017 Springer. https://doi.org/10.1007/978-3-319-63046-5_29
Symbolic verification of event–condition–action rules in intelligent environments
Vannucchi, C., Diamanti, M., Mazzante, G., Cacciagrano, D., Culmone, R., Gorogiannis, N., Mostarda, L. and Raimondi, F. 2017. Symbolic verification of event–condition–action rules in intelligent environments. Journal of Reliable Intelligent Environments. 3 (2), pp. 117-130. https://doi.org/10.1007/s40860-017-0036-z
A novel symbolic approach to verifying epistemic properties of programs
Gorogiannis, N., Raimondi, F. and Boureanu, I. 2017. A novel symbolic approach to verifying epistemic properties of programs. Twenty-Sixth International Joint Conference on Artificial Intelligence. Melbourne, Australia 19 - 25 Aug 2017 International Joint Conferences on Artificial Intelligence. pp. 206-212 https://doi.org/10.24963/ijcai.2017/30
Disproving inductive entailments in separation logic via base pair approximation
Brotherston, J. and Gorogiannis, N. 2015. Disproving inductive entailments in separation logic via base pair approximation. TABLEAUX 2015: 24th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods. Wroclaw, Poland 21 - 24 Sep 2015 Springer. https://doi.org/10.1007/978-3-319-24312-2_20
Model checking for symbolic-heap separation logic with inductive predicates
Brotherston, J., Gorogiannis, N., Kanovich, M. and Rowe, R. 2016. Model checking for symbolic-heap separation logic with inductive predicates. POPL 2016: 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. St. Petersburg, FL, USA 20 - 22 Jan 2016 Association for Computing Machinery (ACM). pp. 84-96 https://doi.org/10.1145/2837614.2837621
Foundations for decision problems in separation logic with general inductive predicates
Antonopoulos, T., Gorogiannis, N., Haase, C., Kanovich, M. and Ouaknine, J. 2014. Foundations for decision problems in separation logic with general inductive predicates. 17th International Conference on the Foundations of Software Science and Computation Structures, FOSSACS 2014. Grenoble, France 05 - 13 Apr 2014 Springer. https://doi.org/10.1007/978-3-642-54830-7_27
Cyclic abduction of inductively defined safety and termination preconditions
Brotherston, J. and Gorogiannis, N. 2014. Cyclic abduction of inductively defined safety and termination preconditions. 21st International Static Analysis Symposium, SAS 2014. Munich, Germany 11 - 13 Sep 2014 Springer. https://doi.org/10.1007/978-3-319-10936-7_5
A generic cyclic theorem prover
Brotherston, J., Gorogiannis, N. and Petersen, R. 2012. A generic cyclic theorem prover. APLAS 2012. https://doi.org/10.1007/978-3-642-35182-2_25
The complexity of abduction for separated heap abstractions
Gorogiannis, N., Kanovich, M. and O’Hearn, P. 2011. The complexity of abduction for separated heap abstractions. SAS 2011. https://doi.org/10.1007/978-3-642-23702-7_7
Merging first-order knowledge using dilation operators
Gorogiannis, N. and Hunter, A. 2008. Merging first-order knowledge using dilation operators. FOIKS 2008. https://doi.org/10.1007/978-3-540-77684-0_11
Requirements, specifications, and minimal refinement
Gorogiannis, N. and Ryan, M. 2002. Requirements, specifications, and minimal refinement. WoLLIC 2002: 9th Workshop on Logic, Language, Information and Computation. Rio de Janeiro, Brazil 30 Jul - 02 Aug 2002 Elsevier. https://doi.org/10.1016/S1571-0661(04)80550-4
Instantiating abstract argumentation with classical logic arguments: postulates and properties
Gorogiannis, N. and Hunter, A. 2011. Instantiating abstract argumentation with classical logic arguments: postulates and properties. Artificial Intelligence. 175 (9-10), pp. 1479-1497. https://doi.org/10.1016/j.artint.2010.12.003
An argument-based approach to reasoning with clinical knowledge
Gorogiannis, N., Hunter, A. and Williams, M. 2009. An argument-based approach to reasoning with clinical knowledge. International Journal of Approximate Reasoning: Uncertainty in Intelligent Systems. 51 (1), pp. 1-22. https://doi.org/10.1016/j.ijar.2009.06.015
Minimal refinements of specifications in modal and temporal logics
Gorogiannis, N. and Ryan, M. 2007. Minimal refinements of specifications in modal and temporal logics. Formal Aspects of Computing. 19 (4), pp. 417-444. https://doi.org/10.1007/s00165-007-0040-9
Implementation of belief change operators using BDDs
Gorogiannis, N. and Ryan, M. 2002. Implementation of belief change operators using BDDs. Studia Logica. 70 (1), pp. 131-156. https://doi.org/10.1023/A:1014610426691
Towards cyber-physical systems as services: the ASIP protocol
Bordoni, M., Bottone, M., Fields, B., Gorogiannis, N., Margolis, M., Primiero, G. and Raimondi, F. 2015. Towards cyber-physical systems as services: the ASIP protocol. 2015 IEEE/ACM 1st International Workshop on Software Engineering for Smart Cyber-Physical Systems (SEsCPS). Florence, Italy 17 - 17 May 2015 IEEE. pp. 52-55 https://doi.org/10.1109/SEsCPS.2015.18
A racket-based robot to teach first-year computer science
Androutsopoulos, K., Gorogiannis, N., Loomes, M., Margolis, M., Primiero, G., Raimondi, F., Varsani, P., Weldin, N. and Zivanovic, A. 2014. A racket-based robot to teach first-year computer science. 7 th European Lisp Symposium. IRCAM, Paris, France 05 - 06 May 2014 pp. 54-61
Instantiating abstract argumentation with classical logic arguments: postulates and properties
Gorogiannis, N. and Hunter, A. 2011. Instantiating abstract argumentation with classical logic arguments: postulates and properties. Artificial Intelligence. 175 (9-10), pp. 1479-1497. https://doi.org/10.1016/j.artint.2010.12.003
Argumentation about treatment efficacy
Gorogiannis, N., Hunter, A., Patkar, V. and Williams, M. 2010. Argumentation about treatment efficacy. Riaño, D., Teije, A., Miksch, S. and Peleg, M. (ed.) KR4HC 2009: International Workshop on Knowledge Representation for Health Care. Verona, Italy 19 Jul 2009 Springer. pp. 169-179 https://doi.org/10.1007/978-3-642-11808-1_14
The complexity of the warranted formula problem in propositional argumentation
Hirsch, R. and Gorogiannis, N. 2010. The complexity of the warranted formula problem in propositional argumentation. Journal of Logic and Computation. 20 (2), pp. 481-499. https://doi.org/10.1093/logcom/exp074
Implementing semantic merging operators using binary decision diagrams
Gorogiannis, N. and Hunter, A. 2008. Implementing semantic merging operators using binary decision diagrams. International Journal of Approximate Reasoning: Uncertainty in Intelligent Systems. 49 (1), pp. 234-251. https://doi.org/10.1016/j.ijar.2008.03.008