Completeness of Pointer Program Verification by Separation Logic

被引：8
|
作者：
Tatsuta, Makoto [1 ]
Chin, Wei-Ngan [2 ]
Al Ameen, Mahmudul Faisal [3 ]
机构：
[1] Natl Inst Informat, 2-1-2 Hitotsubashi, Tokyo 1018430, Japan
[2] Natl Univ Singapore, Dept Comp Sci, Singapore, Singapore
[3] Grad Univ Adv Studies, Dept Informat, Tokyo 1018430, Japan
来源：
SEFM 2009: SEVENTH INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING AND FORMAL METHODS | 2009年
关键词：
HOARE-LOGIC;
D O I：
10.1109/SEFM.2009.33
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
Reynolds' separation logical system for pointer program verification is investigated. This paper proves its completeness theorem as well as the expressiveness theorem that states the weakest precondition of every program and every assertion can be expressed by some assertion. This paper also introduces the predicate that represents the next new cell, and proves the completeness and the soundness of the extended system under deterministic semantics.
引用
收藏
页码：179 / +
页数：2
相关论文
共 50 条
  • [21] Automatic verification of pointer programs using monadic second-order logic
    Jensen, JL
    Jorgensen, ME
    Klarlund, N
    Schwartzbach, MI
    ACM SIGPLAN NOTICES, 1997, 32 (05) : 226 - 234
  • [22] Expressive Completeness of Separation Logic With Two Variables and No Separating Conjunction
    Demri, Stephane
    Deters, Morgan
    PROCEEDINGS OF THE JOINT MEETING OF THE TWENTY-THIRD EACSL ANNUAL CONFERENCE ON COMPUTER SCIENCE LOGIC (CSL) AND THE TWENTY-NINTH ANNUAL ACM/IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS), 2014,
  • [23] Expressive Completeness of Separation Logic with Two Variables and No Separating Conjunction
    Demri, Stephane
    Deters, Morgan
    ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 2016, 17 (02)
  • [24] Enhancing modular OO verification with separation logic
    Chin, Wei-Ngan
    David, Cristina
    Nguyen, Huu Hai
    Qin, Shengchao
    ACM SIGPLAN NOTICES, 2008, 43 (01) : 87 - 99
  • [25] Verification Algorithms for Automated Separation Logic Verifiers
    Eilers, Marco
    Schwerhoff, Malte
    Mueller, Peter
    COMPUTER AIDED VERIFICATION, PT I, CAV 2024, 2024, 14681 : 362 - 386
  • [26] Enhancing Modular OO Verification with Separation Logic
    Chin, Wei-Ngan
    David, Cristina
    Nguyen, Huu Hai
    Qin, Shengchao
    POPL'08: PROCEEDINGS OF THE 35TH ANNUAL ACM SIGPLAN-SIGACT SYMPOSIUM ON PRINCIPLES OF PROGRAMMING LANGUAGES, 2008, : 87 - 99
  • [27] Logic plus control: On program construction and verification
    Drabent, Wlodzimierz
    THEORY AND PRACTICE OF LOGIC PROGRAMMING, 2018, 18 (01) : 1 - 29
  • [28] External Behavior of a Logic Program and Verification of Refactoring
    Fandinno, Jorge
    Hansen, Zachary
    Lierler, Yuliya
    Lifschitz, Vladimir
    Temple, Nathan
    THEORY AND PRACTICE OF LOGIC PROGRAMMING, 2023, 23 (04) : 933 - 947
  • [29] Verifying Pointer Programs Using Separation Logic and Invariant Based Programming in Isabelle
    Preoteasa, Viorel
    INTEGRATED FORMAL METHODS (IFM 2016), 2016, 9681 : 457 - 473
  • [30] Automatic Verification of Heap Manipulation Using Separation Logic
    Berdine, Josh
    SOFSEM 2009-THEORY AND PRACTICE OF COMPUTER SCIENCE, PROCEEDINGS, 2009, 5404 : 34 - 34
12345