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 条

[1] SMT-based context-bounded model checking for CUDA programs
Pereira, Phillipe
Albuquerque, Higo
da Silva, Isabela
Marques, Hendrio
Monteiro, Felipe
Ferreira, Ricardo
Cordeiro, Lucas
[J]. CONCURRENCY AND COMPUTATION-PRACTICE & EXPERIENCE, 2017, 29 (22):
[2] Bounded Model Checking of C plus plus Programs Based on the Qt Framework
Sousa, Felipe R. M.
Cordeiro, Lucas C.
de Lima Filho, Eddie B.
[J]. 2015 IEEE 4TH GLOBAL CONFERENCE ON CONSUMER ELECTRONICS (GCCE), 2015, : 179 - 180
[3] SMT-based model checking for recursive programs
Komuravelli, Anvesh
Gurfinkel, Arie
Chaki, Sagar
[J]. FORMAL METHODS IN SYSTEM DESIGN, 2016, 48 (03) : 175 - 205
[4] SMT-based model checking for recursive programs
Anvesh Komuravelli
Arie Gurfinkel
Sagar Chaki
[J]. Formal Methods in System Design, 2016, 48 : 175 - 205
[5] SMT-Based Model Checking for Recursive Programs
Komuravelli, Anvesh
Gurfinkel, Arie
Chaki, Sagar
[J]. COMPUTER AIDED VERIFICATION, CAV 2014, 2014, 8559 : 17 - 34
[6] SMT-Based Bounded Model Checking for Embedded ANSI-C Software
Cordeiro, Lucas
Fischer, Bernd
Marques-Silva, Joao
[J]. IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 2012, 38 (04) : 957 - 974
[7] SMT-Based Bounded Model Checking for Embedded ANSI-C Software
Cordeiro, Lucas
Fischer, Bernd
Marques-Silva, Joao
[J]. 2009 IEEE/ACM INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING, PROCEEDINGS, 2009, : 137 - 148
[8] Checking RTECTL Properties of STSs via SMT-Based Bounded Model Checking
Zbrzezny, Agnieszka M.
Zbrzezny, Andrzej
[J]. DISTRIBUTED COMPUTING AND ARTIFICIAL INTELLIGENCE, 12TH INTERNATIONAL CONFERENCE, 2015, 373 : 55 - 62
[9] SMT-based Bounded Model Checking for OSEK/VDX Applications
Zhang, Haitao
Aoki, Toshiaki
Lin, Hsin-Hung
Zhang, Min
Chiba, Yuki
Yatake, Kenro
[J]. 2013 20TH ASIA-PACIFIC SOFTWARE ENGINEERING CONFERENCE (APSEC 2013), VOL 1, 2013, : 307 - 314
[10] SMT-Based Bounded Model Checking for Weighted Epistemic ECTL
Zbrzezny, Agnieszka M.
Wozna-Szczesniak, Bozena
Zbrzezny, Andrzej
[J]. PROGRESS IN ARTIFICIAL INTELLIGENCE-BK, 2015, 9273 : 651 - 657

← 1 2 3 4 5 →