Completeness and expressiveness of pointer program verification by separation logic

被引：2
|
作者：
Tatsuta, Makoto [1 ]
Chin, Wei-Ngan [2 ]
Al Ameen, Mahmudul Faisal [2 ]
机构：
[1] Natl Inst Informat, 2-1-2 Hitotsubashi, Tokyo 1018430, Japan
[2] Natl Univ Singapore, Dept Comp Sci, Singapore, Singapore
来源：
INFORMATION AND COMPUTATION | 2019年 / 267卷
关键词：
Hoare's logic; Separation logic; Completeness theorem; Expressiveness theorem; Inductive definitions; AUTOMATED VERIFICATION; HOARE-LOGIC; SHAPE; SIZE;
D O I：
10.1016/j.ic.2019.03.002
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
Reynolds' separation logical system for pointer program verification is investigated. This paper proves its completeness theorem that states that every true asserted program is provable in the logical system. In order to prove the completeness, this paper shows the expressiveness theorem that states the weakest precondition of every program and every assertion can be expressed by some assertion. This paper also introduces an extension of the assertion language with inductive definitions and proves the soundness theorem, the expressiveness theorem, and the completeness theorem. (C) 2019 Elsevier Inc. All rights reserved.
引用
收藏
页码：1 / 27
页数：27
相关论文
共 50 条
  • [1] Completeness of Pointer Program Verification by Separation Logic
    Tatsuta, Makoto
    Chin, Wei-Ngan
    Al Ameen, Mahmudul Faisal
    [J]. SEFM 2009: SEVENTH INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING AND FORMAL METHODS, 2009, : 179 - +
  • [2] EXPRESSIVENESS AND THE COMPLETENESS OF HOARE LOGIC
    BERGSTRA, JA
    TUCKER, JV
    [J]. JOURNAL OF COMPUTER AND SYSTEM SCIENCES, 1982, 25 (03) : 267 - 284
  • [3] Program Verification with Separation Logic
    Iosif, Radu
    [J]. MODEL CHECKING SOFTWARE, SPIN 2018, 2018, 10869 : 48 - 62
  • [4] PROCESS LOGIC - EXPRESSIVENESS, DECIDABILITY, COMPLETENESS
    HAREL, D
    KOZEN, D
    PARIKH, R
    [J]. JOURNAL OF COMPUTER AND SYSTEM SCIENCES, 1982, 25 (02) : 144 - 170
  • [5] Automated verification of pointer programs in pointer logic
    Wang Z.
    Chen Y.
    Wang Z.
    Hua B.
    [J]. Frontiers of Computer Science in China, 2008, 2 (4): : 380 - 397
  • [6] An extension to pointer logic for verification
    Wang, Zhifang
    Chen, Yiyun
    Wang, Zhenming
    Wang, Wei
    Tian, Bo
    [J]. TASE 2008: SECOND IFIP/IEEE INTERNATIONAL SYMPOSIUM ON THEORETICAL ASPECTS OF SOFTWARE ENGINEERING, PROCEEDINGS, 2008, : 49 - +
  • [7] Conditions of expressiveness and completeness for bunches of logic functions
    Kudryavtsev, VV
    [J]. DOKLADY AKADEMII NAUK, 1998, 359 (01) : 16 - 18
  • [8] A Program Construction and Verification Tool for Separation Logic
    Dongol, Brijesh
    Gomes, Victor B. F.
    Struth, Georg
    [J]. MATHEMATICS OF PROGRAM CONSTRUCTION, MPC 2015, 2015, 9129 : 137 - 158
  • [9] Towards mechanized program verification with separation logic
    Weber, T
    [J]. COMPUTER SCIENCE LOGIC, PROCEEDINGS, 2004, 3210 : 250 - 264
  • [10] Epistemic Quantified Boolean Logic: Expressiveness and Completeness Results
    Belardinelli, Francesco
    van der Hoek, Wiebe
    [J]. PROCEEDINGS OF THE TWENTY-FOURTH INTERNATIONAL JOINT CONFERENCE ON ARTIFICIAL INTELLIGENCE (IJCAI), 2015, : 2748 - 2754
12345