# Model Checking C++ Programs

arXiv: https://arxiv.org/abs/2107.01093 · HTML: https://mlsanity.com/paper/2107.01093/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 2 Jul 2021.

## Built on by (most cited first, 3 of 3)

- [A New Era in Software Security: Towards Self-Healing Software via Large Language Models and Formal Verification](https://mlsanity.com/paper/2305.14752/) (2023)
- [UnitTenX: Generating Tests for Legacy Packages with AI Agents Powered by Formal Verification](https://mlsanity.com/paper/2510.05441/) (2025)
- [The 4/δ Bound: Designing Predictable LLM-Verifier Systems for Formal Method Guarantee](https://mlsanity.com/paper/2512.02080/) (2025)

## Abstract (arXiv)

In the last three decades, memory safety issues in system programming languages such as C or C++ have been one of the significant sources of security vulnerabilities. However, there exist only a few attempts with limited success to cope with the complexity of C++ program verification. Here we describe and evaluate a novel verification approach based on bounded model checking (BMC) and satisfiability modulo theories (SMT) to verify C++ programs formally. Our verification approach analyzes bounded C++ programs by encoding into SMT various sophisticated features that the C++ programming language offers, such as templates, inheritance, polymorphism, exception handling, and the Standard C++ Libraries. We formalize these features within our formal verification framework using a decidable fragment of first-order logic and then show how state-of-the-art SMT solvers can efficiently handle that. We implemented our verification approach on top of ESBMC. We compare ESBMC to LLBMC and DIVINE, which are state-of-the-art verifiers to check C++ programs directly from the LLVM bitcode. Experimental results show that ESBMC can handle a wide range of C++ programs, presenting a higher number of correct verification results. At the same time, it reduces the verification time if compared to LLBMC and DIVINE tools. Additionally, ESBMC has been applied to a commercial C++ application in the telecommunication domain and successfully detected arithmetic overflow errors, potentially leading to security vulnerabilities.