ConcuBinE

/ˈkɒŋ.kjə.baɪn/

Concurrent Binary Evaluator - a toolchain for simulating and bounded model checking of random memory access sequences by concurrent programs on a simple virtual machine.

ConcuBinE can be used to symbolically execute arbitrary programs either via simulation, or by solving the resulting bounded model checking problem using state-of-the-art SMT solvers and replaying them for comparison.

      program*
     /       \
simulate    solve
     \       /
       trace
         |
       replay
        |
      graduate

Prerequisites

To build ConcuBinE from source you need:

• Make
• GCC >= 7
• Z3 (C++ API)

To run ConcuBinE, access to supported solvers' executables via $PATH is required:

• Boolector
• CVC4

To build and setup these solvers you can use the scripts setup-{boolector,cvc4,z3}.sh in the scripts directory and set-search-path.sh for adding the required entries to your shells $PATH variable.

Build

git clone https://github.com/phlo/concubine.git

cd concubine

./configure.sh

make

Usage

For a list of command line options, refer to concubine -h.

Documentation

ConcuBinE was developed in the course of a master thesis to evaluate the potential of different encodings for verifying concurrent software with respect to the memory ordering habits of modern hardware. See the thesis for further details.