Documentation

ESBMC is an SMT-based bounded model checker for C, C++, CUDA, CHERI, Python, Solidity, Java and Kotlin. It detects — or proves the absence of — runtime errors and verifies user-defined assertions, without requiring pre- or post-conditions.

New here? Start with Setup, then the Build Guide and Usage.

What ESBMC checks

By default, ESBMC checks for:

• User-specified assertion failures
• Out-of-bounds array access
• Illegal pointer dereferences (null, out-of-bounds, double-free, misalignment)
• Integer overflow
• Floating-point NaN
• Division by zero
• Memory leaks

For concurrent (pthread) programs it can additionally check for deadlock, data races, atomicity violations and lock-ordering issues by explicitly exploring thread interleavings. Each reported violation is annotated with its matching CWE identifier.

Explore the docs

Background theory

To understand how ESBMC reasons about programs, read the background theory:

Further reading

• Slides on detecting software vulnerabilities with ESBMC: Part I, Part II, Part III
• The software security course covers further implementation details about ESBMC.

Support

ESBMC is under active development, with new features, optimizations and encodings added continuously. We invite our users to submit bug reports to the GitHub repository. For any question, reach us via GitHub Discussions or our public ESBMC Zulip Channel.