What Is Decidable in Separation Logic Beyond Progress, Connectivity and Establishment?

被引:0
作者
Bozec, Tanguy [1 ]
Peltier, Nicolas [1 ]
Petitjean, Quentin [2 ]
Sighireanu, Mihaela [2 ]
机构
[1] Univ Grenoble Alpes, LIG, CNRS, F-38000 Grenoble, France
[2] Univ Paris Saclay, Lab Methodes Formelles, ENS Paris Saclay, CNRS, F-91190 Gif Sur Yvette, France
来源
AUTOMATED REASONING, IJCAR 2024, PT II | 2024年 / 14740卷
关键词
Separation logic; Inductive definitions; Bounded treewidth fragment; PCE fragment; Symbolic heaps; Decision procedures;
D O I
10.1007/978-3-031-63501-4_9
中图分类号
TP18 [人工智能理论];
学科分类号
081104 ; 0812 ; 0835 ; 1405 ;
摘要
The predicate definitions in Separation Logic (SL) play an important role: they capture a large spectrum of unbounded heap shapes due to their inductiveness. This expressiveness power comes with a limitation: the entailment problem is undecidable if predicates have general inductive definitions (ID). Iosif et al. [8] proposed syntactic and semantic conditions, called PCE, on the ID of predicates to ensure the decidability of the entailment problem. We provide a (possibly nonterminating) algorithm to transform arbitrary ID into equivalent PCE definitions when possible. We show that the existence of an equivalent PCE definition for a given ID is undecidable, but we identify necessary conditions that are decidable. The algorithm has been implemented, and experimental results are reported on a benchmark, including significant examples from SL-COMP.
引用
收藏
页码:157 / 175
页数:19
相关论文
共 11 条
  • [1] Brotherston James, 2012, APLAS 12, DOI [10.1007/978-3-642-35182-2_25, DOI 10.1007/978-3-642-35182-2_25]
  • [2] Echenim M., 2021, LEIBNIZ INT P INFORM, V183
  • [3] Entailment is Undecidable for Symbolic Heap Separation Logic Formulae with Non-Established Inductive Rules
    Echenim, Mnacho
    Iosif, Radu
    Peltier, Nicolas
    [J]. INFORMATION PROCESSING LETTERS, 2022, 173
  • [4] Unifying Decidable Entailments in Separation Logic with Inductive Definitions
    Echenim, Mnacho
    Iosif, Radu
    Peltier, Nicolas
    [J]. AUTOMATED DEDUCTION, CADE 28, 2021, 12699 : 183 - 199
  • [5] Echenim Mnacho, 2020, P LPAR 20, P191
  • [6] A Complete Decision Procedure for Linearly Compositional Separation Logic with Data Constraints
    Gu, Xincai
    Chen, Taolue
    Wu, Zhilin
    [J]. AUTOMATED REASONING (IJCAR 2016), 2016, 9706 : 532 - 549
  • [7] Iosif Radu, 2013, Automated Deduction - CADE-24. 24th International Conference on Automated Deduction. Proceedings: LNCS 7898, P21, DOI 10.1007/978-3-642-38574-2_2
  • [8] BI as an assertion language for mutable data structures
    Ishtiaq, S
    O'Hearn, PW
    [J]. ACM SIGPLAN NOTICES, 2001, 36 (03) : 14 - 26
  • [9] A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions
    Matheja, Christoph
    Pagel, Jens
    Zuleger, Florian
    [J]. ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 2023, 24 (01)
  • [10] Reynolds JC, 2002, IEEE S LOG, P55, DOI 10.1109/LICS.2002.1029817