Skip to content

Latest commit

 

History

History
68 lines (51 loc) · 2.54 KB

ESBMC.md

File metadata and controls

68 lines (51 loc) · 2.54 KB
Raw

SMT-based bounded model checker that provides bit-precise verification for C/C++ programs

Name:

ESBMC

Application domain/field:

SMT-based model checking Bounded model checking Multi-threaded programs

Type of tool (e.g. model checker, test generator):

Model checker

Expected input thing:

  • C program
  • Possibly a property file or assertions in the code to express properties that should be checked
  • Parameters to indicate the type of analysis that should be done

Expected input format:

. c file and parameters when calling ESBMC. The property file should be in the format used by SV-COMP.

Expected output:

VERIFICATION SUCCESSFUL or VERIFICATION FAILED, followed by more detail about the counterexample that the tool found.

Internals (tools used, frameworks, techniques, paradigms, ...):

ESBMC v6.0 employs a k-induction algorithm to both falsify and prove safety properties in C programs

Some of the parameters/analyses that ESBMC supports are:

  • --k-induction to enable k-induction
  • --floatbv to enable floating-point SMT encoding
  • --interval-analysis, which enables invariant generation
  • --memory-leak-check for memory verification
  • --overflow-check to check for overflows

As back-ends ESBMC supports the following SMT solvers: Boolector, Z3, Yices, MathSAT, CVC4.

ESBMC is based on CBMC.

Comments:

URIs (github, websites, etc.):

Repository: https://github.com/esbmc/esbmc Project page: http://esbmc.org/

Last commit date:

01 Dec 2022 (default branch) 01 Dec 2022 (last activity)

Last publication date:

8 September 2021

List of related papers:

Model checking C++ programs (Software Testing, Verification and Reliability, Vol. 32, Issue 1, '21) ESBMC 6.1: automated test case generation using bounded model checking (Journal on STTT '20) ESBMC v6.0: Verifying C Programs Using k-Induction and Invariant Inference (TACAS '19) ESBMC 5.0: an industrial-strength C model checker (ASE '18) ESBMC 1.22 (TACAS '14)

Related tools (tools mentioned or compared to in the paper):

Meta

:: C :: C++ :: Model checking :: PV4 :: checks safety properties in C programs, can generate invariants :: Source :: https://doi.org/10.1145/3550355.3552426