PV4 ⊧ ESBMCchecks safety properties in C programs, can generate invariants

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

Application domain/field

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

Type of tool

Model checker

Expected input

• 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

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

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.