C and C++
C and C++
C and C++ are ESBMC’s primary frontends, built on Clang/LLVM. ESBMC verifies C (up to C23) and C++ (up to C++20, with selected C++23 features), checking memory safety, arithmetic overflow, pointer safety, concurrency properties, and user assertions — or proving their absence.
To get started, see the Usage guide and the Constructs reference for the verification annotations. The pages below cover C/C++-specific tooling and support.
Which C++ language and STL features ESBMC supports.
What ESBMC’s C++ frontend does not yet handle, and the workarounds.
Maintainer workflow and benchmark tracking for the C++ frontend.
Materialise reached witnesses as runnable CTest cases.
Generate browsable HTML reports of verification results.
Shrink a failing C program to a minimal reproducer.