Repository files navigation

ESBMC (the Efficient SMT-based Context-Bounded Model Checker) is a mature, permissively licensed open-source context-bounded model checker that automatically detects or proves the absence of runtime errors in single- and multi-threaded C, C++, CUDA, CHERI, Kotlin, Python, and Solidity programs. It can automatically verify predefined safety properties (e.g., bounds check, pointer safety, overflow) and user-defined program assertions.

ESBMC supports:

• The Clang compiler as its C/C++/CHERI/CUDA frontend;
• The Soot framework via Jimple as its Java/Kotlin frontend;
• The ast module as itsPython frontend;
• Implements the Solidity grammar production rules as its Solidity frontend;
• Supports IEEE floating-point arithmetic for various SMT solvers.

ESBMC also implements state-of-the-art incremental BMC andk-induction proof-rule algorithms based on Satisfiability Modulo Theories (SMT) and Constraint Programming (CP) solvers.

We provide some background material/publications to help you understand exactly what ESBMC can offer. These are availableonline. For further information about our main components, check the ESBMCarchitecture.

Our main website isesbmc.org.

To compile ESBMC on Ubuntu 24.04 with LLVM 14 and the SMT solver Z3:

sudo apt updatesudo apt-get install -y clang-14 llvm-14 clang-tidy-14 python-is-python3 python3 git ccache unzip wget curl bison flex g++-multilib linux-libc-dev libboost-all-dev libz3-dev libclang-14-dev libclang-cpp-dev cmakegit clone https://github.com/esbmc/esbmc.gitcd esbmcmkdir build && cd buildcmake .. -DENABLE_Z3=1make -j4

To compile ESBMC on Fedora 40 with the latest version of LLVM and the SMT solver Z3:

# Warning, the --allowerasing parameter will also remove incompatible packages to the packages specified belowsudo dnf install --best --allowerasing"@Development Tools" clang llvm llvm-devel clang-tools-extra python3 git ccache unzip wget curl bison flex gcc-c++ glibc-devel glibc-devel.i686 boost-devel boost-devel.i686 z3-devel clang-devel clang-devel.i686 cmake zlib-devel libffi-devel libstdc++-devel libstdc++-devel.i686git clone https://github.com/esbmc/esbmc.gitcd esbmcmkdir build&&cd buildcmake .. -DENABLE_Z3=1 -DZ3_DIR=/usr/include/z3make -j4

To build ESBMC with other operating systems and SMT solvers, please see theBUILDING file.

The user can also download the latest ESBMC binary for Ubuntu and Windows from thereleases page.

ESBMC should compile just fine in FreeBSD as long as the 32-bit libraries are enabled

pkg install git cmake python3 z3 bison flex boost-allwget https://github.com/llvm/llvm-project/releases/download/llvmorg-16.0.0/clang+llvm-16.0.0-amd64-unknown-freebsd13.tar.xz&& mv clang16mkdir build&&cd buildcmake .. -DLLVM_DIR=../clang16 -DClang_DIR=../clang16make -j4

M1/M2/M3/M4 Macs are now supported.

Given the common elements of OS X, run the script. It runs on both ARM and Intel macs. You do need homebrew installed.It creates the build folder, installs the Boolector SMT solver, and makes esbmc available globally. The script supports building the Python frontend as well. Note that the Python frontend is quite early in the support for Python.

 ./build-esbmc-mac.sh

The raw command is given here for reference.

cmake .. -DZ3_DIR=/opt/homebrew/Cellar/z3/4.13.4 -DENABLE_Z3=1 -DC2GOTO_SYSROOT=/Library/Developer/CommandLineTools/SDKs/MacOSX.sdk -DLLVM_DIR=/opt/homebrew/opt/llvm/lib/cmake/llvm -DClang_DIR=/opt/homebrew/opt/llvm/lib/cmake/clangmake -j8make install

FROM node:18-slim## Install dependencies for ESBMC and other build toolsRUN apt-get update && apt-get install -y \    clang-14 \    llvm-14 \    clang-tidy-14 \    python-is-python3 \    python3 \    git \    ccache \    unzip \    wget \    curl \    bison \    flex \    g++-multilib \    linux-libc-dev \    libboost-all-dev \    libz3-dev \    libclang-14-dev \    libclang-cpp-dev \    cmake \    && rm -rf /var/lib/apt/lists/*# Keep the container running with tail -f /dev/nullCMD ["bash", "-c", "tail -f /dev/null"]

Docker compose file:

version: '3.8'services:  esbmc:    platform: linux/amd64    build:      context: .      dockerfile: Dockerfile  # Assuming your Dockerfile is named `Dockerfile`    tty: true    stdin_open: true

The Linux/Amd64 line is very important for virtualizing Amd64. Now do docker-compose up --build. You can then follow the Linux instructions. Make -j16 works well on M2 mac's and beyond.

As an illustrative example to show some of the ESBMC features, consider the following C code:

#include<assert.h>#include<math.h>intmain() {unsignedintN=nondet_uint();doublex=nondet_double();if(x <=0||isnan(x))return0;unsignedinti=0;while(i<N) {x= (2*x);assert(x>0);++i;  }assert(x>0);return0;}

Here, ESBMC is invoked as follows:

$esbmc file.c --k-induction

Wherefile.c is the C program to be checked, and --k-induction selects the k-induction proof rule. The user can choose the SMT solver, property, and verification strategy. Note that you need math.h installed on your system, especially if you run a release version. build-essential typically covers math.h.

For this particular C program, ESBMC provides the following output as the verification result:

*** Checking inductive stepStarting Bounded Model CheckingUnwinding loop 2 iteration 1 file ex5.c line 8 function mainNot unwinding loop 2 iteration 2 file ex5.c line 8 function mainSymex completed in: 0.001s (40 assignments)Slicing time: 0.000s (removed 16 assignments)Generated 2 VCC(s), 2 remaining after simplification (24 assignments)No solver specified; defaulting to BoolectorEncoding remaining VCC(s) using bit-vector/floating-point arithmeticEncoding to solver time: 0.005sSolving with solver Boolector 3.2.0Encoding to solver time: 0.005sRuntime decision procedure: 0.427sBMC program time: 0.435sVERIFICATION SUCCESSFULSolution found by the inductive step (k = 2)

We refer the user to ourdocumentation webpage for further examples of the ESBMC's features.

Boolector is a fast solver and is recommended. To install Boolector, use the following one line command:

git clone --depth=1 --branch=3.2.3 https://github.com/boolector/boolector && cd boolector && ./contrib/setup-lingeling.sh && ./contrib/setup-btor2tools.sh && ./configure.sh --prefix $PWD/../boolector-release && cd build && make -j9 && make install && cd .. && cd ..

Now rerun cmake,

cmake .. -DENABLE_Z3=1 -DENABLE_BOOLECTOR=1 -DBoolector_DIR=<the folder you ran the above command from>/boolector-release

ESBMC supports specifying options through TOML-formatted config files. To use a config file, export an environment variable:

export ESBMC_CONFIG_FILE="path/to/config.toml"

If no environment file is specified, then the default locations will be checked:

• Windows:%userprofile%\esbmc.toml
• UNIX:~/.config/esbmc.toml

If nothing is found, then nothing is loaded. If you set the environment variable tothe empty string, then it disables the entire config file loading process.

export ESBMC_CONFIG_FILE=""

An example of a config file:

interval-analysis =truegoto-unwind =trueunlimited-goto-unwind =truek-induction =truestate-hashing =trueadd-symex-value-sets =truek-step =2floatbv =trueunlimited-k-steps =falsemax-k-step =100memory-leak-check =truecontext-bound =2

ESBMC detects errors in software by simulating a finite prefix of the program execution with all possible inputs. Classes of implementation errors 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 overflows
• Undefined behavior on shift operations
• Floating-point for NaN
• Divide by zero
• Memory leaks

Concurrent software (using the pthread API) is verified by explicitly exploring interleavings, producing one symbolic execution per interleaving. By default, pointer-safety, array-out-of-bounds, division-by-zero, and user-specified assertions 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)
• Atomicity violations at visible assignments
• Lock acquisition ordering

By default, ESBMC performs a "lazy" depth-first search of interleavings -- it can also encode (explicitly) all interleavings into a single SMT formula.

Many SMT solvers are currently supported:

• Z3 4.13+
• Bitwuzla
• Boolector 3.0+
• MathSAT
• CVC4
• CVC5
• 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 there are not insignificant overheads involved.

We provide a short video that explains ESBMC:

https://www.youtube.com/watch?v=uJ5Jn0sxm08&t=2182s

In a workshop between Arm Research and the University of Manchester, this video was delivered as part of a technical talk on exploiting the SAT revolution for automated software verification.

We offer a post-graduate course in software security that explains the internals of ESBMC.

https://ssvlab.github.io/lucasccordeiro/courses/2020/01/software-security/index.html

This course unit introduces students to basic and advanced approaches to formally building verified trustworthy software systems, where trustworthiness comprises five attributes:reliability,availability,safety,resilience andsecurity.

• Charalambous, Y., Tihanyi, N., Jain, R., Sun, Y., Ferrag, M., Cordeiro, L..A New Era in Software Security: Towards Self-Healing Software via Large Language Models and Formal Verification. 6th ACM/IEEE International Conference on Automation of Software Test (AST), 2025.DOI

• Wu, T., Xiong, S., Manino, E., Stockwell, G., Cordeiro, L.:Verifying Components of Arm® Confidential Computing Architecture with ESBMC. In 31st International Symposium on Static Analysis (SAS), pp. 451-462, 2024.DOI

• Farias, B., Menezes, R., de Lima Filho, E., Sun, Y., Cordeiro, L.:ESBMC-Python: A Bounded Model Checker for Python Programs. In ISSTA 2024: Proceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA), pp. 1836-184, 2024.DOIPresentation

• Pirzada, M., Bhayat, A., Cordeiro, L., Reger, G.LLM-Generated Invariants for Bounded Model Checking Without Loop Unrolling. In 39th IEEE/ACM International Conference on Automated Software Engineering (ASE), pp. 1395-1407, 2024.DOIPresentation

• Rafael Menezes, Daniel Moura, Helena Cavalcante, Rosiane de Freitas, Lucas C. Cordeiro .ESBMC-Jimple: verifying Kotlin programs via jimple intermediate representation In ISSTA'22, pp. 777-780, 2022.DOI

• Franz Brauße, Fedor Shmarov, Rafael Menezes, Mikhail R. Gadelha, Konstantin Korovin, Giles Reger, Lucas C. Cordeiro.ESBMC-CHERI: towards verification of C programs for CHERI platforms with ESBMC In ISSTA'22, pp. 773-776, 2022.DOI

• Felipe R. Monteiro, Mikhail R. Gadelha, Lucas C. Cordeiro.Model checking C++ programs. In Softw. Test. Verification Reliab. 32(1), 2022.DOI,Video,Open access.

• Mikhail R. Gadelha, Lucas C. Cordeiro, Denis A. Nicole.An Efficient Floating-Point Bit-Blasting API for Verifying C Programs. In VSTTE, pp. 178-195, 2020.DOI

• Mikhail Y. R. Gadelha, Felipe R. Monteiro, Jeremy Morse, Lucas C. Cordeiro, Bernd Fischer, Denis A. Nicole.ESBMC 5.0: an industrial-strength C model checker. In ASE, pp. 888-891, 2018.DOI

• Jeremy Morse, Lucas C. Cordeiro, Denis A. Nicole, Bernd Fischer.Model checking LTL properties over ANSI-C programs with bounded traces. In Softw. Syst. Model. 14(1), pp. 65-81, 2015.DOI

• Mikhail Y. R. Gadelha, Hussama Ibrahim Ismail, Lucas C. Cordeiro.Handling loops in bounded model checking of C programs via k-induction. In Int. J. Softw. Tools Technol. Transf. 19(1), pp. 97-114, 2017.DOI

• Phillipe A. Pereira, Higo F. Albuquerque, Isabela da Silva, Hendrio Marques, Felipe R. Monteiro, Ricardo Ferreira, Lucas C. Cordeiro.SMT-based context-bounded model checking for CUDA programs. In Concurr. Comput. Pract. Exp. 29(22), 2017.DOI

• Lucas C. Cordeiro, Bernd Fischer, João Marques-Silva.SMT-Based Bounded Model Checking for Embedded ANSI-C Software. In IEEE Trans. Software Eng. 38(4), pp. 957-974, 2012.DOI

• Lucas C. Cordeiro, Bernd Fischer.Verifying multi-threaded software using smt-based context-bounded model checking. In ICSE, pp. 331-340, 2011.DOI

• Distinguished Paper Award at ASE'24
• 35 awards from international competitions on software verification (SV-COMP) and testing (Test-Comp) 2012-2024 at TACAS/FASE (Strength: Bug Finding and Code Coverage).
• Most Influential Paper Award at ASE’23
• Best Tool Paper Award at SBSeg'23
• Best Paper Award at SBESC’15
• Distinguished Paper Award at ICSE’11

Thisvideo describes how to obtain, build and run ESBMC-CHERI on an example.

A pre-compiled binary for Linux is available in the pre-releaseESBMC-CHERI, for othersystems/archs theBUILDING.mddocument explains the necessary installation steps.

ESBMC is open-source software mainly distributed under the Apache License 2.0. It contains a significant amount of other people's software. However, please take a look at the COPYING file to explain who owns what and under what terms it is distributed.

We'd be extremely happy to receive contributions to improve ESBMC (under the terms of the Apache License 2.0). Please file a pull request against the public GitHub repo if you'd like to submit anything. General discussion and release announcements will be made via GitHub. Please post an issue on GitHub and contact us about research or collaboration.

Please review thedeveloper documentation if you want to contribute to ESBMC.

ESBMC is a fork of CBMC v2.9 (2008), the C Bounded Model Checker. The primary differences between the two are describedhere.

ESBMC is a joint project of the Federal University of Amazonas (Brazil), the University of Manchester (UK), the University of Southampton (UK), and the University of Stellenbosch (South Africa).

The ESBMC development was supported by various research funding agencies, including CNPq (Brazil), CAPES (Brazil), FAPEAM (Brazil), EPSRC (UK), Royal Society (UK), British Council (UK), European Commission (Horizon 2020), and companies including ARM, Intel, Motorola Mobility, Nokia Institute of Technology and Samsung. The ESBMC development is currently funded by ARM, EPSRC grantsEP/T026995/1 andEP/V000497/1,Ethereum Foundation,EU H2020 ELEGANT 957286, Intel, Motorola Mobility (through Agreement N° 4/2021),Soteria project awarded by the UK Research and Innovation for the Digital Security by Design (DSbD) Programme, and XC5 Hong Kong Limited.