As a prerequisite, we recommend to install ESBMC on a GNU/Linux operating system. In order to install ESBMC on your machine, you should download the tool archive1 and save it on your disk. After that, you should open the terminal prompt and decompress the archive using the following command:
$tar xfz esbmc.tgz
The ESBMC distribution is split into five directories:
bin: contains a static-binary file of ESBMC;
include: contains the headers for the C++ API;
lib: contains the libesbmc.a, which can be statically linked to a C++ or imported into a python script;
license: contains the ESBMC, Z3 and Boolector licenses;
share: contains our simplified model of the STL library.
ESBMC aims to support all of C99, and detects errors in software by simulating a finite prefix of the program execution with all possible inputs. Classes of problems that can be detected include:
Concurrent software (using the pthread API) is verified by explicit exploration of interleavings, producing one symbolic execution per interleaving. By default, only normal errors will be checked for; one can also specify options to check concurrent programs for:
By default ESBMC performs a ''lazy'' depth first search of interleavings, but can also encode (explicitly) all interleavings into a single SMT formula. Currently, a number of SMT solvers are supported:
In addition, ESBMC can be configured to use the SMTLIB interactive text format with a pipe, to communicate with an arbitrary solver process, although not-insignificant overheads are involved. A limited subset of C++98 is supported too -- a library modeling the STL is also available.
To check all available options of the ESBMC tool, type:
We are still increasing the robustness of ESBMC tool and also implementing new features (e.g., support for verifying concurrent software), more optimizations and experiencing new encodings. For any question about ESBMC, contact