Testing the Satisfiability of Formulas in Separation Logic with Permissions

被引：0
|
作者：
Peltier, Nicolas [1 ]
机构：
[1] Univ Grenoble Alpes, CNRS, LIG, Inria,Grenoble INP, F-38000 Grenoble, France
来源：
AUTOMATED REASONING WITH ANALYTIC TABLEAUX AND RELATED METHODS, TABLEAUX 2023 | 2023年 / 14278卷
关键词：
D O I：
10.1007/978-3-031-43513-3_23
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
We investigate the satisfiability problem for a fragment of Separation Logic (SL) with inductively defined spatial predicates and permissions. We show that the problem is undecidable in general, but decidable under some restrictions on the rules defining the semantics of the spatial predicates. Furthermore, if the satisfiability of permission formulas can be tested in exponential time for the considered permission model then SL satisfiability is Exptime complete.
引用
收藏
页码：427 / 445
页数：19
相关论文
共 50 条
  • [1] Algorithms for Testing Satisfiability Formulas
    Marin Vlada
    [J]. Artificial Intelligence Review, 2001, 15 : 153 - 163
  • [2] Algorithms for testing satisfiability formulas
    Vlada, M
    [J]. ARTIFICIAL INTELLIGENCE REVIEW, 2001, 15 (03) : 153 - 163
  • [3] EXAMINING THE SATISFIABILITY OF THE FORMULAS OF PROPOSITIONAL DYNAMIC LOGIC
    JANOWSKI, T
    [J]. LECTURE NOTES IN COMPUTER SCIENCE, 1989, 349 : 536 - 536
  • [4] ALGORITHMS FOR TESTING THE SATISFIABILITY OF PROPOSITIONAL FORMULAS
    GALLO, G
    URBANI, G
    [J]. JOURNAL OF LOGIC PROGRAMMING, 1989, 7 (01): : 45 - 61
  • [5] Compositional Satisfiability Solving in Separation Logic
    Le, Quang Loc
    [J]. VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION, VMCAI 2021, 2021, 12597 : 578 - 602
  • [6] EufDpll - A Tool to Check Satisfiability of Equality Logic Formulas
    Tveretina, Olga
    Wesselink, Wieger
    [J]. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2009, 225 : 405 - 420
  • [7] Partitioning methods for satisfiability testing on large formulas
    Park, TJ
    Van Gelder, A
    [J]. INFORMATION AND COMPUTATION, 2000, 162 (1-2) : 179 - 184
  • [8] Satisfiability testing for boolean formulas using Δ-trees
    Gutiérrez G.
    De Guzmán I.P.
    Martínez J.
    Ojeda-Aciego M.
    Valverde A.
    [J]. Studia Logica, 2002, 72 (1) : 85 - 112
  • [9] A method to generate formulas for temporal logic satisfiability checkers
    Sekizawa, Toshifusa
    Takai, Toshinori
    Tanabe, Yoshinori
    Takahashi, Koichi
    [J]. ELECTRONICS AND COMMUNICATIONS IN JAPAN PART II-ELECTRONICS, 2007, 90 (11): : 99 - 108
  • [10] Reasoning over Permissions Regions in Concurrent Separation Logic
    Brotherston, James
    Costa, Diana
    Hobor, Aquinas
    Wickerson, John
    [J]. COMPUTER AIDED VERIFICATION, PT II, 2020, 12225 : 203 - 224
12345