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 条
  • [1] Frame Inference for Inductive Entailment Proofs in Separation Logic
    Quang Loc Le
    Sun, Jun
    Qin, Shengchao
    [J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, TACAS 2018, PT I, 2018, 10805 : 41 - 60
  • [2] Labelled cyclic proofs for separation logic
    Galmiche, Didier
    Mery, Daniel
    [J]. JOURNAL OF LOGIC AND COMPUTATION, 2021, 31 (03) : 892 - 922
  • [3] An Efficient Cyclic Entailment Procedure in a Fragment of Separation Logic
    Quang Loc Le
    Le, Xuan-Bach D.
    [J]. FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATION STRUCTURES, FOSSACS 2023, 2023, 13992 : 477 - 497
  • [4] Cyclic proofs of program termination in separation logic
    Brotherston, James
    Bornat, Richard
    Calcagno, Cristiano
    [J]. ACM SIGPLAN NOTICES, 2008, 43 (01) : 101 - 112
  • [5] Cyclic Proofs of Program Termination in Separation Logic
    Brotherston, James
    Bornat, Richard
    Calcagno, Cristiano
    [J]. POPL'08: PROCEEDINGS OF THE 35TH ANNUAL ACM SIGPLAN-SIGACT SYMPOSIUM ON PRINCIPLES OF PROGRAMMING LANGUAGES, 2008, : 101 - 112
  • [6] Failure of cut-elimination in cyclic proofs of separation logic
    Kimura D.
    Nakazawa K.
    Terauchi T.
    Unno H.
    [J]. 1600, Japan Society for Software Science and Technology (37): : 39 - 52
  • [7] Automatic Cyclic Termination Proofs for Recursive Procedures in Separation Logic
    Rowe, Reuben N. S.
    Brotherston, James
    [J]. PROCEEDINGS OF THE 6TH ACM SIGPLAN CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS, CPP'17, 2017, : 53 - 65
  • [8] The Logic of Separation Logic: Models and Proofs
    de Boer, Frank S.
    Hiep, Hans-Dieter A.
    de Gouw, Stijn
    [J]. AUTOMATED REASONING WITH ANALYTIC TABLEAUX AND RELATED METHODS, TABLEAUX 2023, 2023, 14278 : 407 - 426
  • [9] Ribbon Proofs for Separation Logic
    Wickerson, John
    Dodds, Mike
    Parkinson, Matthew
    [J]. PROGRAMMING LANGUAGES AND SYSTEMS, 2013, 7792 : 189 - 208
  • [10] Compositional entailment checking for a fragment of separation logic
    Constantin Enea
    Ondřej Lengál
    Mihaela Sighireanu
    Tomáš Vojnar
    [J]. Formal Methods in System Design, 2017, 51 : 575 - 607
12345