Theta: Modular Model Checker Built For Diverse Algorithm Configurations (Accompanying Artifact)

Theta: Modular Model Checker Built For Diverse Algorithm Configurations

Milán Mondok, Dániel Szekeres, Levente Bajczi, Dániel Kovács, Mihály Dobos-Kovács and Vince Molnár

Paper Abstract

Safety-critical systems require strong correctness guarantees, typically achieved through formal verification such as model checking. Yet, the need for a diversity of input formalisms, easy reconfiguration, and the integration of heterogeneous algorithms make it challenging to build flexible verification frameworks. Existing solutions often rely on external pre-transformations, limiting adaptability and possibly introducing translation errors. Our general approach supports multiple formalisms and structures verification as an adaptable, modular pipeline of algorithms and formal model transformations. This enables systematic composition of components while reducing errors from high-level translations. Our implementation, Theta, is an open-source verification framework offering diverse frontends, configurable analyses, and transformation steps on a formal model. Its modular design supports experimentation, rapid prototyping, and creation of powerful algorithm portfolios.

1. Overview

This artifact accompanies our TACAS 2026 paper on Theta, a modular and extensible model checking framework designed to support diverse verification algorithms and analysis configurations.It provides all components necessary to reproduce, inspect, and analyze the benchmarking experiments presented in the paper.

The experiments were performed using Theta version 6.12.2, publicly available under the corresponding release tag (v6.12.2).

This artifact relies on the BenchExec framework for reliable benchmarking and resource isolation. It includes all benchmarks, configurations, scripts, and results used in the evaluation. In particular, Fig. 8 (b) and (c) and their data can be reproduced.

2. Artifact Structure

Path
Description

binary/
Contains Theta's JAR files, SMT solvers, and required shared libraries.

benchmarks/
All benchmark programs used in the evaluation, with known expected verdicts.

benchexec/
The exact BenchExec version used in the experiments.

results/
Benchmarking result files generated by BenchExec.

get-latest-files.sh
Helper script for locating the most recent result files.

get-portfolios.py
Script to generate quantile plots from the result data.

get-results.py
Script to parse BenchExec outputs and produce the summary tables from the paper.

quantile.tex
TeX file for the quantile plot.

run-all.sh
Main script to execute all benchmark runs.

run-benchmark.sh
Script to execute a single benchmark configuration.

smoke.sh
Script to execute a smoke test configuration.

packages
.deb files of dependencies

Evaluation Suggestion

We provide here all the commands to run inside the virtual machine. For a more step-by-step guide, skip this section and go on to the next ones.

We suggest (for evaluating the artifact) to first try the smoke test, and then only try and reproduce BMC/PLC in full:

unzip theta-artifact.zip
cd theta-artifact
cd packages
sudo dpkg -i *.deb # install requirements
sudo reboot # reboot to allow benchexec's cgroups to be set up

After reboot:

sudo sysctl -w kernel.apparmor_restrict_unprivileged_userns=0
cd theta-artifact
cd binary
source ../smoke.sh # run the smoke test
cd ..
mv results/plc_bmc results/plc_bmc.bak # move results file to BMC/PLC to re-generate it
cd binary/
source ../run-all.sh # run the full benchmark for PLC/BMC, ~1 hour
cd ..
python3 get-results.py # should show a table with the numbers of Fig.8(b) in each cell, with BMC/PLC updated to the new numbers.
./get-latest-files.sh | python3 get-portfolios.py # should create portfolio.csv with data in Fig.8(c)

# optionally
pdflatex quantile.tex # to produce Fig.8(c) in its entirety

3. Installation and Setup

We assume the TACAS'26 VM as our execution environment. Configure it with sufficient CPU and memory resources (16GB RAM, 4 cores).

3.1. Extracting the Artifact

Some systems experience issues when extracting the large Zenodo archive using standard utilities such as unzip.We recommend using p7zip, which reliably handles the archive structure:

7z x theta-artifact.zip

Either install it from apt (apt install p7zip-full), or from our archive's packages folder in the next step. However, we acknowledge how it could be challenging to install the tool to unzip the artifact from within the artifact.

3.2. Setting Up BenchExec, Pandas, etc

The artifact contains a .deb package for the requirements (BenchExec, Pandas, etc). To install:

cd packages
sudo dpkg -i *.deb

After the packages have been installed, restart the VM for BenchExec's cgroups configurations to take effect.

3.3. Adjusting AppArmor Restrictions

To ensure BenchExec can create unprivileged user namespaces, run:

sudo sysctl -w kernel.apparmor_restrict_unprivileged_userns=0

This must be done after every restart. The log files report this problem if it is not done.

4. Running the Experiments

We provide three ways to reproduce the results and evaluate the artifact:

Smoke-test to see if a short configuration can solve some tasks (~15 minutes)

Partial reproduction of any single configuration (~30 minutes)

Full reproduction of all configurations (~290 days of CPU time)

4.1. Running the Smoke Test

Enter the binary folder, then source the smoke.sh file:

cd binary
source ../smoke.sh # run the smoke test

As a result, there should be a logs-smoke folder with the execution log, and a results-smoke folder with the execution results.

4.2. Running the Benchmarks

By default, the artifact is configured for local BenchExec execution. To execute all experiments:

cd binary/
source ../run-all.sh

This command runs all configurations that do not already have corresponding folders in results/. By default, this will be no-op, as the results folder does exist.

To re-run specific configurations, delete their respective result directories before re-executing the script. For example:

mv results/plc_bmc results/plc_bmc.bak

To re-run all configurations (will take a very long time), move/rename or delete the results folder:

mv results results.bak

5. Analyzing Results

5.1. Generating the Summary Table

To reproduce the result tables presented in the paper:

python3 get-results.py

This parses BenchExec results, aggregates configurations, and produces the main summary table.

5.2. Generating Quantile Plots

To create the quantile plots:

./get-latest-files.sh | python3 get-portfolios.py

This retrieves the most recent result files and generates the performance plots used in the paper. As its output, portfolio.csv will be created.

Then, quantile.tex can be used to generate the quantile plot seen in the paper (pdflatex quantile.tex). Necessary packages for this step are not provided in the artifact as the resulting plot is just a visual representation of the reproduced data, and therefore we do not believe it is necessary for the artifact's evaluation, and the required packages can easily be installed (e.g., sudo apt-get install texlive-full).