Reproduction Package for the CAV 2026 submission: "SvLibChecker: A Light-Weight Tool for Software Model Checking"

Reproduction Package for the Paper “SvLibChecker: A Light-Weight Tool for Software Model Checking” Abstract This artifact is a reproduction package for the paper “A Light-Weight Tool for Software Model Checking” which has been accepted at CAV 2026. The CAV paper presents SvLibChecker, a light-weight tool for software model-checking which is ideal for teaching and rapid-prototyping. SvLibChecker implements nine different algorithms for software model-checking, each in around 100 LOC, and many of its algorithms perform similarly to CPAchecker’s, a state-of-the-asrt software model-checker, on the SV-COMP26 SV-LIB benchmarks. THe artifact consists of all executables, input data and results required to reproduce the experiments. In particular, it also contains the original results of the paper and a way to generate the macros and csv’s to generate the plots in the paper from it. We run the experiments using 2 cores and 15 GiB of memory for at most 15 minutes (CPU time). A full reproduction of the experiments requires roughly 30 days of CPU time. For demonstration purposes, a subset of tasks has been selected which should take at most 1 day to complete and will likely finish sooner. To test that everything is working as intended, we provide a configuration that terminates within ~15 minutes. Requirements All the tools in the artifact have been compiled for a x86 architecture, so it will in general not be possible to run them on an ARM chip. In addition, the artifact, when unpacked takes around 700MB of disk space, and requires at least 3 cores and 16 GB of memory to run it properly. The test-set, i.e., the smoketest can be executed with 2 Cores and 6 GB of memory. Since there are usually differences in the instructions between different CPU models, re-building the tools for the specific CPU model may be necessary. When using a VM this is taken care of by the script setup_vm.sh which compiles the tools for the specific CPU model of the VM. In case this does not work take a look at the Known Issues section for more information. For all further requirements, please take a look at the setup_vm.sh script, which installs all required dependencies into the CAV 26 VM and sets up the environment correctly. Contents This artifact contains the following items: README.md: This file. benchmark-defs/*.xml.template: Templates to generate benchmark definition files for running the experiments using BenchExec. tasks/*.xml: Sets of tasks tasks/all.xml: All tasks used to produce the results in the paper. tasks/subset.xml: Subset of the tasks used in the paper. test/test.xml: Few tasks used only for the smoke test of the Artifact. doc: Some documentation about the project in order to make it more reusable data-analysis: Scripts and definitions to produce the CSV files used to generate the plots in the paper. Additionally, they also generate the macros used to generate the tables in the paper. benchmark-utils/*: Benchmarking utils local_config.sh: File with parameters for BenchExec check_configured.sh: File which checks that BenchExec is set up correctly svlibchecker-configs: Configs for SvLibChecker used for the experiments Makefile: Makefile to run the experiments. results-paper: Raw results of the experiments presented in the paper. License.txt: License information for the artifact. sv-benchmarks: The SV-Benchmarks repository with SV-LIB benchmarks in version beee8104aeee08591d8af0d5813ddfa03877bd90. Unnecessary files have been removed to make the artifact smaller. Tools can be found in the tools directory. CPAchecker: CPAchecker version 5bf8b77394d234a58291601b5b951dcedd9f798f. SvLibChecker: SvLibChecker version 47ea213d6c15fb83dcc8b9c048ef50af9391cfe5. This ReadMe contains the following sections to help the user to reproduce the experiments: TL;DR: A quick guide to reproduce the experiments and analyze the data. Environment: Describes the environment in which the artifact was tested and can be run. Experiments: Describes how to execute the experiments and generate the results. Smoke Test: Describes how to run the smoketest and the expected results Results: Describes where the results can be found and how to analyze them. Information for Reuse: Documentation on how to reuse the artifact for other purposes. Known Issues: Describes known issues when executing the artifact. TL;DR Before starting, if you are using a VM make sure to configure it to use at least 3 cores, at least 16GiB of RAM. If you are using vboxmanage on a computer with Linux, this can be done with running VBoxManage modifyvm "MyVM" --cpus 3 --memory 16500. Extract the files in the provided ZIP archive to an arbitrary directory and open a terminal inside it. Execute the script ./setup_vm.sh if you are using the CAV 26 VM to set up the environment correctly, and install all required dependencies. This will restart the VM once. Set the environment variables: source benchmark-utils/local_config.sh: if you have an overlayfs in version 1.10 or newer installed Choose one of the following sets of tasks to run: make setup-benchmark: Reproduce all results in our paper on your machine (takes about 15 days of CPU time, requires 2 cores and 16 GB of RAM). We strongly discourage from running this inside a VM. make setup-subset: Reproduce the results on a representative subset of our tasks (takes ~1 day of CPU time). make setup-test: Smoke test the VM and the setup (takes ~15 min). Run make all-verification to run the verification of all the tools with all their configurations. In case you want to use the paper results execute cp -r results-paper results instead of running the experiments. Run make analyze-results to process the produced results in order to get human-readable results. They can be found in the results/tables directory. The CSV files used to generate the plots in the paper can be found in the output directory. Environment To run the artifact BenchExec, Python >= 3.12, and Java >= 21 are required. Inside a clean VM running Ubuntu 24.04, please see the documentation of the respective tools for installation hints. A non-exhaustive list of required packages: * CPAchecker: Java 21 * SvLibChecker: Python >= 3.12 We recommend running the artifact inside the TACAS 26 VM, Note that both MathSAT and Z3 which are used as SMT solvers inside the tools have been compiled for x86 architecture, and may not work for platforms other than the ones they were compiled for. In case such a problem is encountered, please execute make -B lib/pip inside the tools/svlibchecker directory to recompile MathSAT and Z3 for your architecture. NOTE: We assume that all the following commands are executed from inside the root directory of the artifact! Experiments Setup Run source benchmark-utils/local_config.sh (needs to be repeated every time a new shell is opened). Benchmark Selection Depending on your available resources you can select different sets of benchmarks to execute the tools on. You have the following options: A quick test with two files, which can be useful to test that the artifact is behaving as intended. To select it use make setup-test. Executing this benchmark set should take ~15 minutes. A subset of the tasks used for the benchmarks in the paper. To select it use make setup-subset. Executing this benchmark set should take around 1 day. The full benchmark set used in the experiments. To select it use make setup-benchmark. Executing this benchmark set will take around 15 days of CPU Time. Running the Experiments To run all experiments multiple targets need to be executed one after the other, their list and order can be found in the TL;DR. Each of them encompass multiple targets for the different verifier configurations. All experiments are run using BenchExec in order to ensure reliable benchmarks. Smoke Test To run the smoketest, just follow the instruction in the TL;DR using the test set, which can be configured using make setup-test. Smoke Test Results After running the target make all-verification for the test-set, the output on the command line should be similar to the one provided under doc/smoketest-cli-output.txt. Results The results contain not only the results from the paper, but also additional experiments done with different SMT-Solvers. The SMT-Solver for SvLibChecker is added as a suffix, either *-msat or *-z3 to indicate whether MathSAT or Z3 was used. Generating the Results Once you ran all experiments execute make analyze-results to generate an HTML table which contains the information used for the first three claims. It can be found in the results-paper/tables directory, and contains the results for all tools and configurations. For further information on how to interact with the HTML table, we refer to the BenchExec documentation. The numbers in the table and the quantile plots correspond to those in the paper. Each row in the table corresponds to a task, and each column corresponds to a tool configuration. The cells are colored according to the result of the tool on the task, and they contain the CPU time taken by the tool to solve the task. The command make analyze-results also generates CSV files, and latex macros which can be used to generate the plots and tables in the paper. These are exported into the results directly of the data-analysis directory. We export a lot of different values in the macros file to make it easier to keep the paper up to date with the results, while the CSV files mostly contain the CPU time taken by each tool on each task, to produce the quantile plots for Claim 2. In addition, the information for Claim 3 is contained in the CSV file data-analysis/cache/cloc_results.csv, which contains the data generated by CLOC counting the LOC of the project. Note that the processing of the *.xml.bz2 results into CSV files are cached during the data processing under data-analysis/cache, in order to make the development of the data-analysis