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 条
  • [1] Completeness and expressiveness of pointer program verification by separation logic
    Tatsuta, Makoto
    Chin, Wei-Ngan
    Al Ameen, Mahmudul Faisal
    INFORMATION AND COMPUTATION, 2019, 267 : 1 - 27
  • [2] Program Verification with Separation Logic
    Iosif, Radu
    MODEL CHECKING SOFTWARE, SPIN 2018, 2018, 10869 : 48 - 62
  • [3] Automated verification of pointer programs in pointer logic
    Wang Z.
    Chen Y.
    Wang Z.
    Hua B.
    Frontiers of Computer Science in China, 2008, 2 (4): : 380 - 397
  • [4] An extension to pointer logic for verification
    Wang, Zhifang
    Chen, Yiyun
    Wang, Zhenming
    Wang, Wei
    Tian, Bo
    TASE 2008: SECOND IFIP/IEEE INTERNATIONAL SYMPOSIUM ON THEORETICAL ASPECTS OF SOFTWARE ENGINEERING, PROCEEDINGS, 2008, : 49 - +
  • [5] A Program Construction and Verification Tool for Separation Logic
    Dongol, Brijesh
    Gomes, Victor B. F.
    Struth, Georg
    MATHEMATICS OF PROGRAM CONSTRUCTION, MPC 2015, 2015, 9129 : 137 - 158
  • [6] Towards mechanized program verification with separation logic
    Weber, T
    COMPUTER SCIENCE LOGIC, PROCEEDINGS, 2004, 3210 : 250 - 264
  • [7] Implementation of Pointer Logic for Automated Verification
    Wang, Zhifang
    Chen, Yiyun
    Wang, Zhenming
    Wang, Wei
    Tian, Bo
    PROCEEDINGS OF THE 9TH INTERNATIONAL CONFERENCE FOR YOUNG COMPUTER SCIENTISTS, VOLS 1-5, 2008, : 2295 - +
  • [8] On the Complexity of Pointer Arithmetic in Separation Logic
    Brotherston, James
    Kanovich, Max
    PROGRAMMING LANGUAGES AND SYSTEMS, APLAS 2018, 2018, 11275 : 329 - 349
  • [9] Soundness and Completeness of the NRB Verification Logic
    Breuer, Peter T.
    Pickin, Simon J.
    SOFTWARE ENGINEERING AND FORMAL METHODS, 2014, 8368 : 389 - 404
  • [10] Relative Completeness of Incorrectness Separation Logic
    Lee, Yeonseok
    Nakazawa, Koji
    PROGRAMMING LANGUAGES AND SYSTEMS, APLAS 2024, 2025, 15194 : 264 - 282
12345