Automated Cyclic Entailment Proofs in Separation Logic

被引：0
|
作者：
Brotherston, James [1 ]
Distefano, Dino [2 ]
Petersen, Rasmus Lerchedahl [2 ]
机构：
[1] Univ London Imperial Coll Sci Technol & Med, Dept Comp, London SW7 2AZ, England
[2] Univ London Queen Mary, Dept Comp Sci, London E1 4NS, England
来源：
AUTOMATED DEDUCTION - CADA-23 | 2011年 / 6803卷
基金：
英国工程与自然科学研究理事会;
关键词：
SHAPE-ANALYSIS; VERIFICATION;
D O I：
暂无
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
We present a general automated proof procedure, based upon cyclic proof, for inductive entailments in separation logic. Our procedure has been implemented via a deep embedding of cyclic proofs in the HOL Light theorem prover. Experiments show that our mechanism is able to prove a number of non-trivial entailments involving inductive predicates.
引用
下载
收藏
页码：131 / +
页数：3
相关论文
共 50 条
  • [11] Foundations for Entailment Checking in Quantitative Separation Logic
    Batz, Kevin
    Fesefeldt, Ira
    Jansen, Marvin
    Katoen, Joost-Pieter
    Kessler, Florian
    Matheja, Christoph
    Noll, Thomas
    PROGRAMMING LANGUAGES AND SYSTEMS, ESOP 2022, 2022, 13240 : 57 - 84
  • [12] Compositional entailment checking for a fragment of separation logic
    Enea, Constantin
    Lengal, Ondrej
    Sighireanu, Mihaela
    Vojnar, Tomas
    FORMAL METHODS IN SYSTEM DESIGN, 2017, 51 (03) : 575 - 607
  • [13] Separation Logic Adapted for Proofs by Rewriting
    Myreen, Magnus O.
    INTERACTIVE THEOREM PROVING, PROCEEDINGS, 2010, 6172 : 485 - 489
  • [14] SEMANTIC ENTAILMENT IN NONCLASSICAL LOGICS BASED ON PROOFS FOUND IN CLASSICAL-LOGIC
    CAFERRA, R
    DEMRI, S
    LECTURE NOTES IN ARTIFICIAL INTELLIGENCE, 1992, 607 : 385 - 399
  • [15] Effective Entailment Checking for Separation Logic with Inductive Definitions
    Katelaan, Jens
    Matheja, Christoph
    Zuleger, Florian
    TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PT II, 2019, 11428 : 319 - 336
  • [16] An EXPTIME-Complete Entailment Problem in Separation Logic
    Peltier, Nicolas
    LOGIC, LANGUAGE, INFORMATION, AND COMPUTATION, WOLLIC 2024, 2024, 14672 : 157 - 174
  • [17] A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions
    Matheja, Christoph
    Pagel, Jens
    Zuleger, Florian
    ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 2023, 24 (01)
  • [18] Cyclic Proofs, Hypersequents, and Transitive Closure Logic
    Das, Anupam
    Girlando, Marianna
    AUTOMATED REASONING, IJCAR 2022, 2022, 13385 : 509 - 528
  • [19] Decidable entailment checking for concurrent separation logic with fractional permissions
    Lee Y.
    Nakazawa K.
    Computer Software, 2023, 40 (04) : 67 - 86
  • [20] Automated Termination Proofs for Logic Programs by Term Rewriting
    Schneider-Kamp, Peter
    Giesl, Juergen
    Serebrenik, Alexander
    Thiemann, Rene
    ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 2009, 11 (01)
12345