ESBMC: An Efficient SMT-based Bounded Model Checker
line decor
line decor

NEW!16/01/2018: ESBMC-kind won the Bronze Medal in the overall ranking at SV-COMP 2018.


NEW! 22/01/2016: ESBMC v2.1 won one gold and one silver medal in the 5th International Competition on Software Verification (SV-COMP 2016).


NEW! 12/11/2015: ESBMC v2.1.0 for Linux released.

ESBMC is a context-bounded model checker for embedded C/C++ software based on Satisfiability Modulo Theories (SMT). Its development started in 2008 on top of the CProver framework [1], but almost all components have been re-designed and re-implemented in subsequent years, including the basic data structures, frontend, symbolic execution, memory model, and back-end. ESBMC allows the verification engineer (i) to verify single- and multi-threaded software (with shared variables and locks); (ii) to reason about arithmetic under- and overflow, pointer safety, memory leaks, array bounds, atomicity and order violations, deadlock and data race; (iii) to verify programs that make use of bit-level, pointers, structs, unions and fixed- and (IEEE) floating-point arithmetic.

ESBMC does not require the user to annotate the programs with pre/post-conditions, but allows the user to state additional properties using assert-statements, that are then checked as well. It also provides three approaches (lazy, schedule recording, and underapproximation and widening) to model check multi-threaded software. ESBMC can be invoked through the command-line interface or configured through the Eclipse plug-in. ESBMC converts the verification conditions using different background theories and passes them directly to an SMT solver. In addition, ESBMC can output verification conditions using the SMT logics QF_AUFBV and QF_AUFLIRA. A demonstration video is available here.

ESBMC uses the SMT solvers Boolector (Default), Z3, MathSAT, Yices, and CVC4, which are also included in the distribution. The restrictions of those SMT solvers and CPROVER licenses apply.

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

ESBMC source code is available in a public github repository:

For further information about ESBMC, please send an e-mail to

You should also read the ESBMC license.

[1] This product includes software developed by Daniel Kroening, ETH Zurich and Edmund Clarke, Computer Science Department, Carnegie Mellon University.