Reproduction Package for CAV 2025 Article `Btor2-Select: Machine Learning Based Algorithm Selection for Hardware Model Checking'

Abstract This artifact is a reproduction package for the article “Btor2-Select: Machine Learning Based Algorithm Selection for Hardware Model Checking”, published at CAV 2025. The artifact has been evaluated and awarded the badges of Available, Functional, and Reusable. It is archived on Zenodo with the DOI 10.5281/zenodo.15485472. The paper investigates machine-learning-based algorithm selection for hardware model checking in the Btor2 language. It proposes a framework to train an algorithm selector that predicts the best available off-the-shelf model checker for a given verification task. The selector then invokes the predicted backend model checker to solve the task. This artifact supports the reproduction of: the training of the algorithm selector using the provided performance data and the evaluation of the algorithm selector (integrated with backend model checkers) against state-of-the-art hardware model checkers. The artifact consists of source code, precompiled executables, and input data used in the training and evaluation of the paper, as well as the results produced from the experiments. Specifically, it includes the selector trained by our framework, the backend verifiers to be selected, a set of Btor2 verification tasks collected for training and evaluation, the experimental data generated from the evaluation, and instructions to run the tools and experiments. Artifact Requirements This reproduction package works best with the SoSy-Lab Virtual Machine, which runs Ubuntu 24.04 LTS and has all the required dependencies installed. If you test the artifact with this VM, you do not need to install any package. Please login the VM as user vagrant via GUI or SSH. The VM has been tested with VirtualBox 7.0 on a Linux (Ubuntu 24.04) computer. The benchmarking framework BenchExec used in our experiments relies on control groups and namespaces provided by modern Linux kernels. Our tool, Btor2-Select, was tested with Python 3.12. Additionally, one of the compared tools, super_prove, is executed in a containerized environment with Podman (tested with version 4.9.3). To perform most of the experiments included in this artifact, a machine with 16 GB of RAM, 4 CPU cores, and 15 GB of disk space is needed. A full reproduction of the training part required around 8.5 hours of wall-clock time on a server equipped with 2 TB of RAM and two 2.0 GHz AMD EPYC 7713 CPUs, each with 128 processing units. The evaluation phase consumed more than 776 hours of CPU time on machines with 3.4 GHz processors. For demonstration purposes, a subset of benchmark tasks can be used. Training on a subset of 450 Btor2 tasks took approximately less than a minute, while evaluation on 30 selected simple Btor2 tasks took roughly 5 minutes on a standard laptop. This artifact README includes time estimates for the various commands referenced throughout. The uncompressed package takes around 14 GB of disk space. Please make sure there is enough disk space available before extracting it. If you only want to run experiments on the bit-vector tasks, you can exclude the directory perf-eval-hwmc/benchmarks/array when unzipping the package. Contents This artifact contains the following items: README.{html,md}: this documentation (we recommend viewing the HTML version with a browser) LICENSE.txt: license information of the artifact btor2-select/: the machine-learning-based framework for algorithm selection and the trained selector (our open-source project, at commit b6505455) bin/: contains the executables of Btor2-Select and Btor2-Para (a parallel portfolio constructed for evaluating Btor2-Select) btor2select/: contains the main production codes for Btor2-Select, including: btor2_select.py: performs inference using the trained selector and executes the selected backend model checker train.py: trains the proposed algorithm selector cross_validation.py: conducts cross-validation analysis Other supporting scripts for different ML models, e.g., PWC-SVM-BoKW, PWC-SVM-WL data/demo/: a small collection of Btor2 verification tasks and their performance data, intended for use in a training demo. README: for additional information perf-eval-hwmc: a directory for evaluating performance of backend model checkers, consisting of: benchmarks/: a set of Btor2 verification tasks collected for training and evaluation dataset/: the performance dataset used for training verifiers/: tool archives of several backend model checkers (including both hardware and software verifiers) benchexec/: a checkout of BenchExec, a reliable benchmarking framework with precise resource management, used to perform the evaluation bench-defs/: benchmark definitions used by BenchExec README: for further information data-submission/: a directory containing the raw and processed data obtained from our experiments cross_val/: the cross-validation results evaluation/: the evaluation results of Btor2-Select, Btor2-Para, ABC, AVR, rIC3, and super_prove paper-results/: the results presented in the paper demo-results/: the results of the demo runs Makefile: a file that assembles commands for running experiments and processing data

Fetched live from OpenAlex and de-inverted. Abstracts are not stored in this database: the inverted indexes are 8.6 GB of the frame’s 9.3 GB of text, and the host has 13 GB free.