More Web Proxy on the site http://driver.im/

research-article

The Bernays-Schönfinkel-Ramsey Class of Separation Logic with Uninterpreted Predicates

Authors:

Mnacho Echenim,

Nicolas PeltierAuthors Info & Claims

ACM Transactions on Computational Logic (TOCL), Volume 21, Issue 3

Article No.: 19, Pages 1 - 46

https://doi.org/10.1145/3380809

Published: 02 March 2020 Publication History

Abstract

This article investigates the satisfiability problem for Separation Logic with k record fields, with unrestricted nesting of separating conjunctions and implications. It focuses on prenex formulæ with a quantifier prefix in the language ∃*∀* that contain uninterpreted (heap-independent) predicate symbols. In analogy with first-order logic, we call this fragment Bernays-Schönfinkel-Ramsey Separation Logic [BSR(SL^k)]. In contrast with existing work on Separation Logic, in which the universe of possible locations is assumed to be infinite, we consider both finite and infinite universes in the present article. We show that, unlike in first-order logic, the (in)finite satisfiability problem is undecidable for BSR(SL^k). Then we define two non-trivial subsets thereof, for which the finite and infinite satisfiability problems are PSPACE-complete, respectively, assuming that the maximum arity of the uninterpreted predicate symbols does not depend on the input. These fragments are defined by controlling the polarity of the occurrences of separating implications, as well as the occurrences of universally quantified variables within their scope. These decidability results have natural applications in program verification, as they allow to automatically prove lemmas that occur in, e.g., entailment checking between inductively defined predicates and validity checking of Hoare triples expressing partial correctness conditions.

References

[1]

Timos Antonopoulos, Nikos Gorogiannis, Christoph Haase, Max Kanovich, and Joël Ouaknine. 2014. Foundations for decision problems in separation logic with general inductive predicates. In Foundations of Software Science and Computation Structures, Anca Muscholl (Ed.). Springer, Berlin, 411--425.

[2]

Sanjeev Arora and Boaz Barak. 2009. Computational Complexity—A Modern Approach. Cambridge University Press.

Digital Library

[3]

Egon Börger, Erich Grädel, and Yuri Gurevich. 1997. The Classical Decision Problem. Springer.

[4]

James Brotherston, Dino Distefano, and Rasmus L. Petersen. 2011. Automated cyclic entailment proofs in separation logic. In Proceedings of the 23rd International Conference on Automated Deduction (CADE-23). Springer, Berlin, 131--146.

[5]

James Brotherston, Carsten Fuhs, Juan A. Navarro Pérez, and Nikos Gorogiannis. 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’14) and the 29th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS’14) (CSL-LICS’14). ACM, Article 25, 25:1--25:10 pages.

Digital Library

[6]

Cristiano Calcagno, Philippa Gardner, and Matthew Hague. 2005. From separation logic to first-order logic. In Foundations of Software Science and Computational Structures. Springer, Berlin, 395--409.

[7]

Cristiano Calcagno, Hongseok Yang, and Peter W. O’Hearn. 2001. Computability and complexity results for a spatial assertion language for data structures. In Proceedings of the Conference on Foundations of Software Technology and Theoretical Computer Science (FST TCS’01). Springer, Berlin, 108--119.

[8]

Stéphane Demri and Morgan Deters. 2016. Expressive completeness of separation logic with two variables and no separating conjunction. ACM Trans. Comput. Log. 17, 2 (2016), 12:1--12:44.

Digital Library

[9]

Stéphane Demri, Étienne Lozes, and Alessio Mansutti. 2018. The effects of adding reachability predicates in propositional separation logic. In Proceedings of the 21st International Conference FOSSACS’18 held as part of the European Joint Conferences on Theory and Practice of Software, Foundations of Software Science and Computation Structures (ETAPS’18) (Lecture Notes in Computer Science), Christel Baier and Ugo Dal Lago (Eds.), Vol. 10803. Springer, 476--493.

[10]

Mnacho Echenim, Radu Iosif, and Nicolas Peltier. 2019. Prenex separation logic with one selector field. In Proceedings of the 28th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX’19) (Lecture Notes in Computer Science), Serenella Cerrito and Andrei Popescu (Eds.), Vol. 11714. Springer, 409--427.

[11]

P. Erdós and R. Rado. 1952. Combinatorial theorems on classifications of subsets of a given set. Proc. Lond. Math. Soc. s3--2, 1 (1952), 417--439.

[12]

Pascal Fontaine. 2007. Combinations of theories and the Bernays-Schönfinkel-ramsey class. In Proceedings of 4th International Verification Workshop in connection with (CADE-21) (CEUR Workshop Proceedings), Bernhard Beckert (Ed.), Vol. 259. CEUR-WS.org.

[13]

Radu Iosif, Adam Rogalewicz, and Jiri Simacek. 2013. The tree width of separation logic with recursive definitions. In Proceedings of the Conference on Automated Deduction (CADE-24), LNCS, Vol. 7898. Springer.

Digital Library

[14]

Samin S. Ishtiaq and Peter W. O’Hearn. 2001. BI as an assertion language for mutable data structures. In ACM SIGPLAN Notices, Vol. 36. ACM, 14--26.

[15]

Jens Katelaan, Christoph Matheja, and Florian Zuleger. 2019. Effective entailment checking for separation logic with inductive definitions. In Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’19) held as part of the European Joint Conferences on Theory and Practice of Software (ETAPS’19), Part II (Lecture Notes in Computer Science), Tomás Vojnar and Lijun Zhang (Eds.), Vol. 11428. Springer, 319--336.

[16]

Quang Loc Le, Makoto Tatsuta, Jun Sun, and Wei-Ngan Chin. 2017. A decidable fragment in separation logic with inductive predicates and arithmetic. In Proceedings of the 29th International Conference on Computer Aided Verification - (CAV 2017), Part II (Lecture Notes in Computer Science), Rupak Majumdar and Viktor Kuncak (Eds.), Vol. 10427. Springer, 495--517.

[17]

Harry R. Lewis. 1980. Complexity results for classes of quantificational formulas. J. Comput. Syst. Sci. 21, 3 (1980), 317--353.

[18]

Etienne Lozes. 2004. Separation logic preserves the expressive power of classical logic. In Proceedings of the 2nd Workshop on Semantics, Program Analysis, and Computing Environments for Memory Management (SPACE’04).

[19]

Peter W. O’Hearn, John C. Reynolds, and Hongseok Yang. 2001. Local reasoning about programs that alter data structures. In Proceedings of the 15th International Workshop on Computer Science Logic CSL’01 and the 10th Annual Conference of the European Association for Computer Science Logic (EACSL’01). 1--19.

[20]

C. H. Papadimitriou. 1994. Computational Complexity. Addison-Wesley.

[21]

F. P. Ramsey. 1987. On a problem of formal logic. Classic Papers in Combinatorics (1987), 1--24.

[22]

Andrew Reynolds, Radu Iosif, and Cristina Serban. 2017. Reasoning in the Bernays-Schönfinkel-Ramsey fragment of separation logic. In Verification, Model Checking, and Abstract Interpretation, Ahmed Bouajjani and David Monniaux (Eds.). Springer International Publishing, Cham, 462--482.

[23]

John C. Reynolds. 2002. Separation logic: A logic for shared mutable data structures. In Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science (LICS’02). IEEE Computer Society, 55--74.

Digital Library

[24]

Walter J. Savitch. 1970. Relationships between nondeterministic and deterministic tape complexities. J. Comput. Syst. Sci. 4, 2 (1970), 177--192.

Digital Library

[25]

Moshe Y. Vardi. 1982. The complexity of relational query languages. In Proceedings of the 14th Annual ACM Symposium on Theory of Computing. ACM, 137--146.

Cited By

Lee YNakazawa K(2024)Relative Completeness of Incorrectness Separation LogicProgramming Languages and Systems10.1007/978-981-97-8943-6_13(264-282)Online publication date: 23-Oct-2024
https://dl.acm.org/doi/10.1007/978-981-97-8943-6_13
Dacík TRogalewicz AVojnar TZuleger F(2024)Deciding Boolean Separation Logic via Small ModelsTools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-031-57246-3_11(188-206)Online publication date: 4-Apr-2024
https://doi.org/10.1007/978-3-031-57246-3_11
de Boer FHiep Hde Gouw S(2023)The Logic of Separation Logic: Models and ProofsAutomated Reasoning with Analytic Tableaux and Related Methods10.1007/978-3-031-43513-3_22(407-426)Online publication date: 14-Sep-2023
https://doi.org/10.1007/978-3-031-43513-3_22
Show More Cited By

Index Terms

The Bernays-Schönfinkel-Ramsey Class of Separation Logic with Uninterpreted Predicates
1. Theory of computation
  1. Logic

Recommendations

A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions
We develop a doubly exponential decision procedure for the satisfiability problem of guarded separation logic—a novel fragment of separation logic featuring user-supplied inductive predicates, Boolean connectives, and separating connectives, including ...
The Effects of Adding Reachability Predicates in Quantifier-Free Separation Logic
The list segment predicate ls used in separation logic for verifying programs with pointers is well suited to express properties on singly-linked lists. We study the effects of adding ls to the full quantifier-free separation logic with the separating ...
Two-Variable Separation Logic and Its Inner Circle

Separation logic is a well-known assertion language for Hoare-style proof systems. We show that first-order separation logic with a unique record field restricted to two quantified variables and no program variables is undecidable. This is among the ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Transactions on Computational Logic

ACM Transactions on Computational Logic Volume 21, Issue 3

July 2020

407 pages

ISSN:1529-3785

EISSN:1557-945X

DOI:10.1145/3384674

Editor:
Orna Kupferman
School of Computer Science and Engineering, Hebrew University, Israel

Issue’s Table of Contents

Copyright © 2020 ACM.

Permission to make digital or hard copies of all or part 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 components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 02 March 2020

Accepted: 01 December 2019

Revised: 01 December 2019

Received: 01 July 2019

Published in TOCL Volume 21, Issue 3

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

5
Total Citations
View Citations
117
Total Downloads

Downloads (Last 12 months)6
Downloads (Last 6 weeks)1

Reflects downloads up to 15 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Lee YNakazawa K(2024)Relative Completeness of Incorrectness Separation LogicProgramming Languages and Systems10.1007/978-981-97-8943-6_13(264-282)Online publication date: 23-Oct-2024
https://dl.acm.org/doi/10.1007/978-981-97-8943-6_13
Dacík TRogalewicz AVojnar TZuleger F(2024)Deciding Boolean Separation Logic via Small ModelsTools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-031-57246-3_11(188-206)Online publication date: 4-Apr-2024
https://doi.org/10.1007/978-3-031-57246-3_11
de Boer FHiep Hde Gouw S(2023)The Logic of Separation Logic: Models and ProofsAutomated Reasoning with Analytic Tableaux and Related Methods10.1007/978-3-031-43513-3_22(407-426)Online publication date: 14-Sep-2023
https://doi.org/10.1007/978-3-031-43513-3_22
Batz KFesefeldt IJansen MKatoen JKeßler FMatheja CNoll T(2022)Foundations for Entailment Checking in Quantitative Separation LogicProgramming Languages and Systems10.1007/978-3-030-99336-8_3(57-84)Online publication date: 29-Mar-2022
https://doi.org/10.1007/978-3-030-99336-8_3
Demri SLozes EMansutti A(2021)The Effects of Adding Reachability Predicates in Quantifier-Free Separation LogicACM Transactions on Computational Logic10.1145/344826922:2(1-56)Online publication date: 21-Jun-2021
https://dl.acm.org/doi/10.1145/3448269

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

HTML Format

View this article in HTML Format.

Media

Figures

Other

Tables

View Issue’s Table of Contents