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 条
  • [41] Cyclic Proofs of Program Termination in Separation Logic
    Brotherston, James
    Bornat, Richard
    Calcagno, Cristiano
    POPL'08: PROCEEDINGS OF THE 35TH ANNUAL ACM SIGPLAN-SIGACT SYMPOSIUM ON PRINCIPLES OF PROGRAMMING LANGUAGES, 2008, : 101 - 112
  • [42] Cyclic proofs of program termination in separation logic
    Brotherston, James
    Bornat, Richard
    Calcagno, Cristiano
    ACM SIGPLAN NOTICES, 2008, 43 (01) : 101 - 112
  • [43] Expressive completeness by separation for discrete time interval temporal logic with expanding modalities
    Guelev, Dimitar P.
    Moszkowski, Ben
    INFORMATION PROCESSING LETTERS, 2024, 186
  • [44] Relaxed Separation Logic: A Program Logic for C11 Concurrency
    Vafeiadis, Viktor
    Narayan, Chinmay
    ACM SIGPLAN NOTICES, 2013, 48 (10) : 867 - 883
  • [45] On Completeness of Logic Programs
    Drabent, Wlodzimierz
    LOGIC-BASED PROGRAM SYNTHESIS AND TRANSFORMATION (LOPSTR 2014), 2015, 8981 : 261 - 278
  • [46] Completeness of neighbourhood logic
    Barua, R
    Roy, S
    Zhou, CC
    JOURNAL OF LOGIC AND COMPUTATION, 2000, 10 (02) : 271 - 295
  • [47] COMPLETENESS OF QUANTUM LOGIC
    STACHOW, EW
    JOURNAL OF PHILOSOPHICAL LOGIC, 1976, 5 (02) : 237 - 280
  • [48] Proving completeness by logic
    Escoffier, B
    Paschos, VT
    INTERNATIONAL JOURNAL OF COMPUTER MATHEMATICS, 2005, 82 (02) : 151 - 161
  • [49] Completeness of Subtrilattice Logic
    Kamide, Norihiro
    2020 IEEE 50TH INTERNATIONAL SYMPOSIUM ON MULTIPLE-VALUED LOGIC (ISMVL 2020), 2020, : 279 - 284
  • [50] COMPLETENESS IN LOGIC OF QUESTIONS
    HARRAH, D
    AMERICAN PHILOSOPHICAL QUARTERLY, 1969, 6 (02) : 158 - 164
12345