ESBMC

An Efficient SMT-based Bounded Model Checker.

GitHub

Documentation
News
Publications
SV-COMP
People
Applications
Download Archive
Third Party Contributions

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:

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:

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:

$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.