Separation Logic Verification of C Programs with an SMT Solver

被引：10

作者：

Botincan, Matko ^{[1
]}

Parkinson, Matthew ^{[2
]}

Schulte, Wolfram ^{[3
]}

机构：

[1] Univ Zagreb, Zagreb, Croatia

[2] Univ Cambridge, Cambridge, England

[3] Microsoft Res, Redmond, WA USA

来源：

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE | 2009年 / 254卷

关键词：

Separation logic; automated verification; automated theorem proving; C programming language;

D O I：

10.1016/j.entcs.2009.09.057

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

This paper presents a methodology for automated modular verification of C programs against specifications written in separation logic. The distinguishing features of the approach are representation of the C memory model in separation logic by means of rewrite rules suitable for automation and the careful integration of an SMT solver behind the separation logic prover to guide the proof search.

引用

页码：5 / 23

页数：19

共 50 条

[1] A Verification Framework for Assembly Programs Under Relaxed Memory Model Using SMT Solver
Maleehuan, Pattaravut
Chiba, Yuki
Aoki, Toshiaki
[J]. IEICE TRANSACTIONS ON INFORMATION AND SYSTEMS, 2018, E101D (12): : 3038 - 3058
[2] Predicting SMT Solver Performance for Software Verification
Healy, Andrew
Monahan, Rosemary
Power, James F.
[J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2017, (240): : 20 - 37
[3] SPEN: A Solver for Separation Logic
Enea, Constantin
Lengal, Ondrej
Sighireanu, Mihaela
Vojnar, Tomas
[J]. NASA FORMAL METHODS (NFM 2017), 2017, 10227 : 302 - 309
[4] A Decision Procedure for Separation Logic in SMT
Reynolds, Andrew
Iosif, Radu
Serban, Cristina
King, Tim
[J]. AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, ATVA 2016, 2016, 9938 : 244 - 261
[5] Verification of logic programs
Pedreschi, D
Ruggieri, S
[J]. JOURNAL OF LOGIC PROGRAMMING, 1999, 39 (1-3): : 125 - 176
[6] Applying an SMT Solver to Coverage-Driven Design Verification
Hamaguchi, Kiyoharu
[J]. IEICE TRANSACTIONS ON FUNDAMENTALS OF ELECTRONICS COMMUNICATIONS AND COMPUTER SCIENCES, 2018, E101A (07): : 1053 - 1056
[7] Scalable Verification of Border Gateway Protocol Configurations with an SMT Solver
Weitz, Konstantin
Woos, Doug
Torlak, Emina
Ernst, Michael D.
Krishnamurthy, Arvind
Tatlock, Zachary
[J]. ACM SIGPLAN NOTICES, 2016, 51 (10) : 765 - 780
[8] GNT -: A solver for disjunctive logic programs
Janhunen, T
Niemelä, I
[J]. LOGIC PROGRAMMING AND NONMONOTONIC REASONING, PROCEEDINGS, 2004, 2923 : 331 - 335
[9] eclingo : A Solver for Epistemic Logic Programs
Cabalar, Pedro
Fandinno, Jorge
Garea, Javier
Romero, Javier
Schaub, Torsten
[J]. THEORY AND PRACTICE OF LOGIC PROGRAMMING, 2020, 20 (06) : 834 - 847
[10] SFLP: a solver for functional logic programs
Hamada, M
Ida, T
[J]. PROCEEDINGS OF THE FIFTH JOINT CONFERENCE ON INFORMATION SCIENCES, VOLS 1 AND 2, 2000, : 466 - 469

← 1 2 3 4 5 →