Documentation

First things first, download the lastest version of ESBMC for Linux OS here. ESBMC is hosted on GitHub.

Installing ESBMC

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 Features

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:

• User specified assertion failures;
• Out of bounds array access;
• Illegal pointer dereferences, such as:
• Dereferencing null;
• Performing an out-of-bounds dereference;
• Double-free of malloc'd memory;
• Misaligned memory access;
• Integer overows;
• Divide by zero;
• Memory leak;

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:

• Deadlock (only on pthread mutexes and conditional variables);
• Data races (i.e., competing writes);

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:

• Z3 4.0+;
• Boolector 2.0+;
• MathSAT;
• CVC4;
• Yices 2.2+;

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:

$esbmc --help

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 esbmc@googlegroups.com.