Benchmarks for Comparing Binary-Level Symbolic Execution Speed

This dataset contains a reproducible computing environment as well as a set of synthetic benchmark applications for comparing symbolic execution speed at the binary level of several symbolic execution engines supporting the 32-bit RISC-V architecture. Specifically, the dataset compares and supports the following engines:

BinSec

angr

SymEx-VP

BinSym

The benchmarks are designed to be easily extendable through the utilization of Guix (a functional package manager for long-term reproducible research). Currently, the supported engines perform IR-based symbolic execution using binary lifting (BinSec & angr) and direct symbolic execution of RISC-V machine code (SymEx-VP & BinSym). The dataset compares these approaches by fully exploring synthetic benchmark applications (e.g. sorting algorithms) with unconstrained symbolic input values and calculating an arithmetic mean over multiple executions, which is then represented as a table and a plot.

More information on using the dataset is available in the supplementary README file.