SMT-Based Bounded Model Checking of C plus plus Programs

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

Research output: Other contributionpeer-review


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 languageEnglish
Publication statusPublished - 2013


  • Software engineering
  • formal methods
  • verification
  • model checking


Dive into the research topics of 'SMT-Based Bounded Model Checking of C plus plus Programs'. Together they form a unique fingerprint.

Cite this