ESBMC is a context-bounded model checker for embedded C/C++ software based on Satisfiability Modulo Theories (SMT) solver. It 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-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. ESBMC is built on top of the CProver framework. ESBMC uses the SMT solvers Z3 (default) and Boolector, which are also included in the distribution. The restrictions of the Z3, Boolector and CProver licenses apply.

References in zbMATH (referenced in 8 articles )

Showing results 1 to 8 of 8.
Sorted by year (citations)

  1. Andrianov, P. S.: Analysis of correct synchronization of operating system components (2020)
  2. Beyer, Dirk; Dangl, Matthias; Wendler, Philipp: A unifying view on SMT-based software verification (2018)
  3. Fedyukovich, Grigory; Sharygina, Natasha: Towards completeness in bounded model checking through automatic recursion depth detection (2015)
  4. Abdulla, Parosh Aziz; Atig, Mohamed Faouzi; Rezine, Othmane; Stenman, Jari: Budget-bounded model-checking pushdown systems (2014)
  5. Fischer, Bernd; Inverso, Omar; Parlato, Gennaro: Cseq: a sequentialization tool for C. (Competition contribution) (2013) ioport
  6. Morse, Jeremy; Cordeiro, Lucas; Nicole, Denis; Fischer, Bernd: Handling unbounded loops with ESBMC 1.20. (Competition contribution) (2013) ioport
  7. Cordeiro, Lucas; Morse, Jeremy; Nicole, Denis; Fischer, Bernd: Context-bounded model checking with ESBMC 1.17 (competition contribution) (2012) ioport
  8. Morse, Jeremy; Cordeiro, Lucas; Nicole, Denis; Fischer, Bernd: Context-bounded model checking of LTL properties for ANSI-C software (2011) ioport