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 条
  • [41] Efficient SMT-Based Model Checking for Signal Temporal Logic
    Lee, Jia
    Yu, Geunyeol
    Bae, Kyungmin
    2021 36TH IEEE/ACM INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING ASE 2021, 2021, : 343 - 354
  • [42] Model Checking of C plus plus Programs Under the x86-TSO Memory Model
    Still, Vladimir
    Barnat, Jiri
    FORMAL METHODS AND SOFTWARE ENGINEERING, ICFEM 2018, 2018, 11232 : 124 - 140
  • [43] An SMT-based approach to satisfiability checking of MITL
    Bersani, Marcello M.
    Rossi, Matteo
    San Pietro, Pierluigi
    INFORMATION AND COMPUTATION, 2015, 245 : 72 - 97
  • [44] Dynamically Checking Ownership Policies in Concurrent C/C plus plus Programs
    Martin, Jean-Phillipe
    Hicks, Michael
    Costa, Manuel
    Akritidis, Periklis
    Castro, Miguel
    ACM SIGPLAN NOTICES, 2010, 45 (01) : 457 - 470
  • [45] Dynamically Checking Ownership Policies in Concurrent C/C plus plus Programs
    Martin, Jean-Phillipe
    Hicks, Michael
    Costa, Manuel
    Akritidis, Periklis
    Castro, Miguel
    POPL'10: PROCEEDINGS OF THE 37TH ANNUAL ACM SIGPLAN-SIGACT SYMPOSIUM ON PRINCIPLES OF PROGRAMMING LANGUAGES, 2010, : 457 - 470
  • [46] Invariant Checking for SMT-Based Systems with Quantifiers
    Redondi, Gianluca
    Cimatti, Alessandro
    Griggio, Alberto
    Mcmillan, Kenneth L.
    ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 2024, 25 (04)
  • [47] SMT-based Software Model Checking: An Experimental Comparison of Four Algorithms
    Beyer, Dirk
    Dangl, Matthias
    VERIFIED SOFTWARE: THEORIES, TOOLS, AND EXPERIMENTS, VSTTE 2016, 2016, 9971 : 181 - 198
  • [48] SMT-Based Symbolic Model-Checking for Operator Precedence Languages
    Chiari, Michele
    Geatti, Luca
    Gigante, Nicola
    Pradella, Matteo
    COMPUTER AIDED VERIFICATION, PT I, CAV 2024, 2024, 14681 : 387 - 408
  • [49] Model Checking of C and C plus plus with DIVINE 4
    Baranova, Zuzana
    Barnat, Jiri
    Kejstova, Katarina
    Kucera, Tadeas
    Lauko, Henrich
    Mrazek, Jan
    Rockai, Petr
    Still, Vladimir
    AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS (ATVA 2017), 2017, 10482 : 201 - 207
  • [50] On the Combination of Polyhedral Abstraction and SMT-Based Model Checking for Petri Nets
    Amat, Nicolas
    Berthomieu, Bernard
    Dal Zilio, Silvano
    APPLICATION AND THEORY OF PETRI NETS AND CONCURRENCY (PETRI NETS 2021), 2021, 12734 : 164 - 185
12345