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

共 23 条

[1] Alexander R. T., 2002, ISSRE, P207
[2] [Anonymous], 2007, The calculus of computation: decision procedures with applications to verification
[3] Bounded model checking of software using SMT solvers instead of SAT solvers
Armando A.
Mantovani J.
Platania L.
[J]. International Journal on Software Tools for Technology Transfer, 2009, 11 (01) : 69 - 83
[4] Barrett C, 2007, LECT NOTES COMPUT SC, V4590, P298
[5] Bounded model checking
Biere, Armin
[J]. Frontiers in Artificial Intelligence and Applications, 2009, 185 (01) : 457 - 481
[6] Blanc N., 2007, IEEE/ACM Conference on Automated software engineering, P521
[7] Brummayer R, 2009, LECT NOTES COMPUT SC, V5505, P174, DOI 10.1007/978-3-642-00768-2_16
[8] Cimatti A., 2010, FMCAD, P121
[9] A tool for checking ANSI-C programs
Clarke, E
Kroening, D
Lerda, F
[J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PROCEEDINGS, 2004, 2988 : 168 - 176
[10] 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

← 1 2 3 →