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 条
  • [31] Modular Verification of Heap Reachability Properties in Separation Logic
    Ter-Gabrielyan, Arshavir
    Summers, Alexander J.
    Mueller, Peter
    PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2019, 3 (OOPSLA):
  • [32] Separation Logic Verification of C Programs with an SMT Solver
    Botincan, Matko
    Parkinson, Matthew
    Schulte, Wolfram
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2009, 254 (5-23) : 5 - 23
  • [33] A pointer logic and certifying compiler
    Chen Y.
    Ge L.
    Hua B.
    Li Z.
    Liu C.
    Wang Z.
    Front. Comput. Sci. China, 2007, 3 (297-312): : 297 - 312
  • [34] The pointer assertion logic engine
    Moller, A
    Schwartzbach, MI
    ACM SIGPLAN NOTICES, 2001, 36 (05) : 221 - 231
  • [35] Reasoning about data-parallel pointer programs in a modal extension of separation logic
    Nishimura, Susumu
    ALGEBRAIC METHODOLOGY AND SOFTWARE TECHNOLOGY, PROCEEDINGS, 2006, 4019 : 293 - 307
  • [36] Automated Quantum Program Verification in Dynamic Quantum Logic
    Takagi, Tsubasa
    Canh Minh Do
    Ogata, Kazuhiro
    DYNAMIC LOGIC. NEW TRENDS AND APPLICATIONS, DALI 2023, 2024, 14401 : 68 - 84
  • [37] An intelligent safety verification based on a paraconsistent logic program
    Nakamatsu, K
    Akama, S
    Abe, JM
    KNOWLEDGE-BASED INTELLIGENT INFORMATION AND ENGINEERING SYSTEMS, PT 2, PROCEEDINGS, 2005, 3682 : 708 - 715
  • [38] USE OF HIGHER-ORDER LOGIC IN PROGRAM VERIFICATION
    ERNST, GW
    HOOKWAY, RJ
    IEEE TRANSACTIONS ON COMPUTERS, 1976, 25 (08) : 844 - 851
  • [39] Verification of Imperative Programs by Constraint Logic Program Transformation
    De Angelis, Emanuele
    Fioravanti, Fabio
    Pettorossi, Alberto
    Proietti, Maurizio
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2013, (129): : 186 - 210
  • [40] Verification of parameterized systems using logic program transformations
    Roychoudhury, A
    Kumar, KN
    Ramakrishnan, CR
    Ramakrishnan, IV
    Smolka, SA
    TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, 2000, 1785 : 172 - 187
12345