PV4 ⊧ ESBMCchecks safety properties in C programs, can generate invariantsSMT-based bounded model checker that provides bit-precise verification for C/C++ programs
- SMT-based model checking
- Bounded model checking
- Multi-threaded programs
Type of toolModel checker
- 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
. c file and parameters when calling ESBMC.
The property file should be in the format used by SV-COMP.
VERIFICATION SUCCESSFUL or
VERIFICATION FAILED, followed by more detail about the counterexample that the tool found.
InternalsESBMC 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-inductionto enable k-induction
--floatbvto enable floating-point SMT encoding
--interval-analysis, which enables invariant generation
--memory-leak-checkfor memory verification
--overflow-checkto check for overflows