A Program Construction and Verification Tool for Separation Logic

被引：13
|
作者：
Dongol, Brijesh [1 ]
Gomes, Victor B. F. [2 ]
Struth, Georg [2 ]
机构：
[1] Brunel Univ, Dept Comp Sci, Uxbridge UB8 3PH, Middx, England
[2] Univ Sheffield, Dept Comp Sci, Sheffield S10 2TN, S Yorkshire, England
来源：
MATHEMATICS OF PROGRAM CONSTRUCTION, MPC 2015 | 2015年 / 9129卷
关键词：
CONCURRENCY;
D O I：
10.1007/978-3-319-19797-5_7
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
An algebraic approach to the design of program construction and verification tools is applied to separation logic. The control-flow level is modelled by power series with convolution as separating conjunction. A generic construction lifts resource monoids to assertion and predicate transformer quantales. The data domain is captured by concrete store-heap models. These are linked to the separation algebra by soundness proofs. Verification conditions and transformation or refinement laws are derived by equational reasoning within the predicate transformer quantale. This separation of concerns makes an implementation in the Isabelle/HOL proof assistant simple and highly automatic. The resulting tool is itself correct by construction; it is explained on three simple examples.
引用
收藏
页码：137 / 158
页数：22
相关论文
共 50 条
  • [1] Program Verification with Separation Logic
    Iosif, Radu
    [J]. MODEL CHECKING SOFTWARE, SPIN 2018, 2018, 10869 : 48 - 62
  • [2] 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 - +
  • [3] Towards mechanized program verification with separation logic
    Weber, T
    [J]. COMPUTER SCIENCE LOGIC, PROCEEDINGS, 2004, 3210 : 250 - 264
  • [4] Logic plus control: On program construction and verification
    Drabent, Wlodzimierz
    [J]. THEORY AND PRACTICE OF LOGIC PROGRAMMING, 2018, 18 (01) : 1 - 29
  • [5] Completeness and expressiveness of pointer program verification by separation logic
    Tatsuta, Makoto
    Chin, Wei-Ngan
    Al Ameen, Mahmudul Faisal
    [J]. INFORMATION AND COMPUTATION, 2019, 267 : 1 - 27
  • [6] Program Verification Under Weak Memory Consistency Using Separation Logic
    Vafeiadis, Viktor
    [J]. COMPUTER AIDED VERIFICATION, CAV 2017, PT I, 2017, 10426 : 30 - 46
  • [7] A DYNAMIC LOGIC FOR PROGRAM VERIFICATION
    HEISEL, M
    REIF, W
    STEPHAN, W
    [J]. LECTURE NOTES IN COMPUTER SCIENCE, 1989, 363 : 134 - 145
  • [8] A program logic for resource verification
    Aspinall, D
    Beringer, L
    Hofmann, M
    Loidl, HW
    Momigliano, A
    [J]. THEOREM PROVING IN HIGHER ORDER LOGICS, PROCEEDINGS, 2004, 3223 : 34 - 49
  • [9] Verification of protocol specifications with separation logic
    Kiss, Tibor
    Craciun, Florin
    Pary, Bazil
    [J]. 2015 IEEE 11TH INTERNATIONAL CONFERENCE ON INTELLIGENT COMPUTER COMMUNICATION AND PROCESSING (ICCP), 2015, : 109 - 116
  • [10] On Automated Program Construction and Verification
    Berghammer, Rudolf
    Struth, Georg
    [J]. MATHEMATICS OF PROGRAM CONSTRUCTION, PROCEEDINGS, 2010, 6120 : 22 - +
12345