ESBMC is an open-source, permissively licensed, context-bounded model checker based on satisfiability modulo theories for verifying 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.

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

News

04/11/2024: Our paper LLM-Generated Invariants for Bounded Model Checking Without Loop Unrolling has received the ACM Distinguished Paper Award at the 39th IEEE/ACM International Conference on Automated Software Engineering (ASE 2024).

25/09/2024: ESBMC v7.7 for Windows and Linux platforms.

06/02/2024: Our paper ESBMC v7.4: Harnessing the Power of Intervals (Competition Contribution) has been accepted at TACAS 2024.

06/02/2024: ESBMC has successfully participated at the 13th Intl. Competition on Software Verification held at TACAS 2024 in Luxembourg. We are in fourth place among 30 state-of-the-art software verifiers at SV-COMP 2024!

Download

You can download the latest ESBMC version from GitHub

Conference Releases

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

Bibtex Entry

If you cite ESBMC >= version 7.4, please use the competition paper at TACAS 2024 (BibTex) as listed below:

@InProceedings{esbmc2024,
    author    = {Rafael Menezes and
                 Mohannad Aldughaim and
                 Bruno Farias and
                 Xianzhiyu Li and
                 Edoardo Manino and
                 Fedor Shmarov and 
	         Kunjian Song and
	         Franz Brauße and 
	         Mikhail R. Gadelha and
	         Norbert Tihanyi and
	         Konstantin Korovin and
	         Lucas C. Cordeiro},
    title     = {{ESBMC} 7.4: {H}arnessing the {P}ower of {I}ntervals},
    booktitle = {$30^{th}$ International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'24)},
    series       = {Lecture Notes in Computer Science},
    volume       = {14572},
    pages     = {376–380},
    doi       = {https://doi.org/10.1007/978-3-031-57256-2_24},
    year      = {2024},
    publisher = {Springer}
}

License

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.