An Efficient SMT-based Bounded Model Checker


Download Archive
Third Party Contributions
Index of Benchmarks

ESBMC is an open source, permissively licensed, context-bounded model checker based on satisfiability modulo theories for the verification of single- and multi-threaded C/C++ programs. It does not require the user to annotate the programs with pre- or postconditions, but allows the user to state additional properties using assert-statements, that are then checked as well. Furthermore, ESBMC provides two approaches (lazy and schedule recording) to model check multi-threaded programs. It converts the verification conditions using different background theories and passes them directly to an SMT solver. In addition, ESBMC provides C++ and Python APIs to access to the internals of ESBMC, allowing inspection and extension at any stage of the verification process.

ESBMC is a joint project with the Federal University of Amazonas, University of Bristol, University of Manchester, University of Stellenbosch, and University of Southampton.


21/02/2019: Our paper ESBMC v6.0: Verifying C Programs using k-Induction and Invariant Inference has been accepted at TACAS 2019.

11/12/2018: ESBMC v6.0.0 for Linux released.

16/11/2018: ESBMC-kind won the Bronze Medal in the overall ranking at SV-COMP 2019.


esbmc-v6.0.0 (last update: 11/12/2018)

Conference Releases

NEW! We provide all tools, scripts, benchmark dataset, and results of our experimental evaluation reported in our IEEE Access 2019 paper here.


Find the documentation of ESBMC’s public C and Python APIs here.

Bibtex Entry

If you cite ESBMC >= version 5.0, please use the tool paper in ASE 2018 (BibTex) as listed below:

    author    = {Mikhail R. Gadelha and
                 Felipe R. Monteiro and
                 Jeremy Morse and
                 Lucas C. Cordeiro and
                 Bernd Fischer and
                 Denis A. Nicole},
    title     = {{ESBMC} 5.0: An Industrial-Strength {C} Model Checker},
    booktitle = {$33^{rd}$ ACM/IEEE Int. Conf. on Automated Software Engineering (ASE'18)},
    pages     = {888--891},
    doi       = {10.1145/3238147.3240481},
    year      = {2018},
    publisher = {ACM},
    address   = {New York, NY, USA}


ESBMC is hosted on GitHub.

You should also read the ESBMC license.

Technical Support

Please use the ESBMC issue tracker for bug reports. For questions, comments or information on new releases, please use our Google group.