SMT-Based Bounded Model Checking of C plus plus Programs

被引：19

作者：

Ramalho, Mikhail ^{[1
]}

Freitas, Mauro ^{[1
]}

Sousa, Felipe ^{[1
]}

Marques, Hendrio ^{[1
]}

Cordeiro, Lucas ^{[1
]}

Fischer, Bernd ^{[2
,3
]}

机构：

[1] Univ Fed Amazonas, Elect & Informat Res Ctr, Manaus, Amazonas, Brazil

[2] Univ Southampton, Southampton SO9 5NH, Hants, England

[3] Univ Stellenbosch, Dept Comp Sci, ZA-7600 Stellenbosch, South Africa

来源：

2013 20TH ANNUAL IEEE INTERNATIONAL CONFERENCE AND WORKSHOPS ON THE ENGINEERING OF COMPUTER BASED SYSTEMS (ECBS 2013) | 2013年

关键词：

Software engineering; formal methods; verification; model checking;

D O I：

10.1109/ECBS.2013.15

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

Bounded model checking of C++ programs presents greater challenges than that of C programs due to the more complex features that the language offers, such as templates, containers, and exception handling. We present ESBMC++, a bounded model checker for C++ programs. It is based on an operational model, an abstract representation of the standard C++ libraries that conservatively approximates their semantics. ESBMC++ uses this to encode the verification conditions using different background theories supported by an SMT solver. Our experimental results show that our approach can handle a wider range of the C++ constructs than existing approaches and substantially reduces the verification time.

引用

页码：147 / 156

页数：10

共 50 条

[21] Summary of Model Checking C plus plus Programs
Monteiro, Felipe R.
Gadelha, Mikhail R.
Cordeiro, Lucas C.
2022 IEEE 15TH INTERNATIONAL CONFERENCE ON SOFTWARE TESTING, VERIFICATION AND VALIDATION (ICST 2022), 2022, : 461 - 461
[22] Model checking C plus plus programs with exceptions
Rockai, P.
Barnat, J.
Brim, L.
SCIENCE OF COMPUTER PROGRAMMING, 2016, 128 : 68 - 85
[23] SMT-Based Software Model Checking
Cimatti, Alessandro
MODEL CHECKING SOFTWARE, 2010, 6349 : 1 - 3
[24] Counterexample Generation for Markov Chains Using SMT-Based Bounded Model Checking
Braitling, Bettina
Wimmer, Ralf
Becker, Bernd
Jansen, Nils
Abraham, Erika
FORMAL TECHNIQUES FOR DISTRIBUTED SYSTEMS, 2011, 6722 : 75 - 89
[25] Checking WELTLK Properties of Weighted Interpreted Systems via SMT-Based Bounded Model Checking
Zbrzezny, Agnieszka M.
Zbrzezny, Andrzej
PRIMA 2015: PRINCIPLES AND PRACTICE OF MULTI-AGENT SYSTEMS, 2015, 9387 : 660 - 669
[26] An SMT-Based Approach to Bounded Model Checking of Designs in State Transition Matrix
Kong, Weiqiang
Shiraishi, Tomohiro
Katahira, Noriyuki
Watanabe, Masahiko
Katayama, Tetsuro
Fukuda, Akira
IEICE TRANSACTIONS ON INFORMATION AND SYSTEMS, 2011, E94D (05): : 946 - 957
[27] Improved SMT-based bounded model checking for real-time systems
Xu L.
Ruan Jian Xue Bao/Journal of Software, 2010, 21 (07): : 1491 - 1502
[28] SMT-Based Bounded Model Checking of Fixed-Point Digital Controllers
Bessa, Iury
Abreu, Renato
Edgar Filho, Joao
Cordeiro, Lucas
IECON 2014 - 40TH ANNUAL CONFERENCE OF THE IEEE INDUSTRIAL ELECTRONICS SOCIETY, 2014, : 295 - 301
[29] SMT-Based Nonlinear PDDL plus Planning
Bryce, Daniel
Gao, Sicun
Musliner, David
Goldman, Robert
PROCEEDINGS OF THE TWENTY-NINTH AAAI CONFERENCE ON ARTIFICIAL INTELLIGENCE, 2015, : 3247 - 3253
[30] SMT-Based Reachability Checking for Bounded Time Petri Nets
Polrola, Agata
Cybula, Piotr
Meski, Artur
FUNDAMENTA INFORMATICAE, 2014, 135 (04) : 467 - 482

← 1 2 3 4 5 →