KestRel is a tool for automatically constructing aligned product programs for relational verification. It uses e-graphs to represent a space of possible product alignments between two programs, and finds desirable product programs through a variety of configurable extraction techniques. The generated product programs may then be given to various off-the-shelf non-relational verifiers.

KestRel requires the following system libraries and utilites:

• Clang for C parsing and compiling.
• Coin CBC for mixed-integer linear programming extraction. At the time of writing, these dependencies can be installed on Debian-based Linux distributions via apt-get install coinor-cbc coinor-libcbc-dev
• Daikon for invariant detection, including the Kvasir Daikon frontend for C.
• Dafny for Houdini-style invariant inference and certain verification pipelines.
• Java Runtime Environment for running Daikon.
• SeaHorn for certain verification pipelines.

KestRel is written in Rust, and manages its library dependencies with Cargo.

Build KestRel using Cargo from the KestRel root directory:

cargo build

You may use cargo-run to execute the verification pipeline on single input files. For example, the following command runs loop counting extraction on the antonopoulous/simple.c benchmark, outputting a prodcut program suitable for verification with SeaHorn:

cargo run -- --input benchmarks/antonopoulos/simple.c count-loops

To use simulated annealing based extraction, include invariant inference, and output the product program in Dafny:

cargo run -- --input benchmarks/antonopoulos/simple.c --infer-invariants --output-mode dafny sa

To see all available KestRel options, run KestRel with the --help flag:

cargo run -- --help

Note you can also invoke the binary directly once it has been built by cargo:

target/debug/kestrel --help

The bin directory contains various scripts for running KestRel experiments.

• bin/run-alignments.sh runs outputs alignments for a group of benchmarks. It optionally takes three arguments: benchmark group, extraction techique, and output mode. For example, bin/run-alignments.sh barthe count-loops dafny runs all benchmarks in the barthe directory using count-loops extraction and outputs Dafny. The first and second argument default to all, which outputs alignments for each possibility. The third argument defaults to seahorn output.

• bin/verify-seahorn.sh runs SeaHorn on all alignments output by bin/run-alignments.sh. It is meant to be run from inside the SeaHorn Docker image.

Coming soon!

Containerization of KestRel with its dependencies is available via a Docker image.

Coming soon!

To build the docker image from scratch, first make sure you have the following dependencies installed:

• Docker
• BuildX. This likely comes with modern Docker client installations. You can check by running docker buildx and verifying you see a usage help message. Building KestRel via the deprecated docker build may also work, but has not been explicitly tested.

To build the KestRel image, run the following command in the KestRel root directory:

docker buildx build -t kestrel .

Once the image exists on your machine, you may run an interactive shell by saying:

docker run -it --ulimit nofile=262144:262144 kestrel

(Note the increased file descriptor limit -- invariant inference may fail without this.)

See the docker run documentation for more ways to use the image.