esbmc
- ESBMC, the efficient SMT based model checker, is a software verification tool for C and C++ code bases. The technique is sound but incomplete -- an error found by esbmc will be correct (modulo errors in the tool), but a successful verification does not guarantee there are no errors.