SMT-Based Bounded Model Checking of C plus plus Programs

Mikhail Ramalho; Mauro Freitas; Felipe Sousa; Hendrio Marques; Lucas Cordeiro; Bernd Fischer

doi:10.1109/ECBS.2013.15

SMT-Based Bounded Model Checking of C plus plus Programs

Mikhail Ramalho, Mauro Freitas, Felipe Sousa, Hendrio Marques, Lucas Cordeiro, Bernd Fischer

Formal Methods

Research output: Other contribution › peer-review

Abstract

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

Original language	English
DOIs	https://doi.org/10.1109/ECBS.2013.15
Publication status	Published - 2013

Keywords

Software engineering
formal methods
verification
model checking

Access to Document

10.1109/ECBS.2013.15

Cite this

@misc{0b5805cf63fc4647a88b023ae51c58b0,

title = "SMT-Based Bounded Model Checking of C plus plus Programs",

abstract = "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",

keywords = "Software engineering, formal methods, verification, model checking",

author = "Mikhail Ramalho and Mauro Freitas and Felipe Sousa and Hendrio Marques and Lucas Cordeiro and Bernd Fischer",

year = "2013",

doi = "10.1109/ECBS.2013.15",

language = "English",

type = "Other",

}

TY - GEN

T1 - SMT-Based Bounded Model Checking of C plus plus Programs

AU - Ramalho, Mikhail

AU - Freitas, Mauro

AU - Sousa, Felipe

AU - Marques, Hendrio

AU - Cordeiro, Lucas

AU - Fischer, Bernd

PY - 2013

Y1 - 2013

N2 - 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

AB - 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

KW - Software engineering

KW - formal methods

KW - verification

KW - model checking

U2 - 10.1109/ECBS.2013.15

DO - 10.1109/ECBS.2013.15

M3 - Other contribution

ER -

SMT-Based Bounded Model Checking of C plus plus Programs

Abstract

Keywords

Access to Document

Fingerprint

Cite this