Reproduction Package for the CAV 2026 submission "Transition Invariants Revisited: Termination Witnesses and Their Validation"

Reproduction Package for the Paper “Transition Invariants Revisited: Termination Witnesses and Their Validation” Abstract This artifact is a reproduction package for the paper “Transition Invariants Revisited: Termination Witnesses and Their Validation” which has been accepted at CAV 2026. The CAV article presents a format for termination witnesses based on transition invariants. In the first part of the paper, we show how to transform usual termination arguments like ranking functions or safety invariants of liveness-to-safety reduction approaches to transition invariants. We implemented the construction based on ranking functions in CPAchecker, and the liveness-to-safety reduction with witness construction in TransVer with CPAchecker, UAutomizer and Goblint as backend verifiers. In the second part of the paper, we present three validation approaches. One is based on liveness-to-safety reduction implemented in TransVer with CPAchecker and UAutomizer as backends. The additional two approaches are based on SMT encoding and are implemented in CPAchecker. This artifact supports the reproduction of the experiments in the CAV article, which evaluated how effectively and efficiently can the produced witnesses from the mentioned verifiers be validated by the mentioned validators. 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 recommend to use CAV 2026 Virtual Machine for this reproduction. 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 40 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 ~30 minutes. Contents This artifact contains the following items: README.md: this documentation benchmark-defs/*.xml.template: templates to generate benchmark definition files for running the experiments using BenchExec benchmark-defs/set_tasks.py: a script to change the tasks to be run in the xml files tasks/*.xml: sets of tasks tasks/all-verifier.xml: all the tasks used to produce the results in the paper for the verifiers natively supporting termination, i.e. CPAchecker tasks/all-transformation.xml: all the tasks used to produce the results in the paper for the verifiers supporting reachability, i.e. CPAchecker, UAutomizer and Goblint, after transforming the termination tasks to reachability using TransVer. This excludes subsets of tasks which cannot be transformed to reachability using TransVer, for example, those using the Heap. tasks/subset.xml: a subset of the tasks used in the paper test/test.xml: a few tasks used only for the smoke test of the artifact 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 config.sh: a file with the parameters for BenchExec check_configured.sh: a file which checks that BenchExec is set up correctly metaval*: the configurations for MetaVal for benchmarking Makefile: Makefile to run the experiments results-paper: raw results of the experiments presented in the paper License.txt: the license information for the artifact sv-benchmarks: SV-COMP26 benchmarks Tools, all under the tools folder, with the following structure: CPAchecker: CPAchecker at commit e34f92b9 in the folder cpachecker UAutomizer: UAutomizer in its SV-COMP26 version in the folder uautomizer Goblint: Goblint in its SV-COMP26 version in the folder goblint TransVer: TransVer at commit d0c5f085 in the folder transver using CPAchecker at commit 96904d63 MetaVal at commit 4579d954 in the folder metaval using TransVer in the commit given above, and CPAchecker and UAuomizer in their SV-COMP26 versions. 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: the environment in which the artifact was tested and can be run Experiments: a description of how to execute the experiments and generate the results Smoke Tests: a description of how to execute the smoke tests Results: an explanation of where the results can be found and how to analyze them Information for Reuse: an explanation of how to apply the verifiers and validators to an arbitrary set of programs, and how to extend the artifact with new tools Known Issues: known issues when executing the artifact TL;DR Run Experiments 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. (Only if you are using the CAV 2026 Virtual Machine) Run setup_vm.sh to install all required dependencies and reboot the VM. Set the environment variables: source benchmark-utils/config_vm.sh: if full read/write access for all tools to /home is fine source benchmark-utils/config.sh: if you have a overlayfs in version 1.10 or newer installed (This is the case in the CAV 2026 Virtual Machine) Choose one of the following sets of tasks to run: make setup-test: smoke test the VM and the setup (takes ~30 minutes) (more information) make setup-subset: reproduce the results on a representative subset of our tasks (takes ~1 day) make setup-benchmark: reproduce all results in our paper on your machine (takes about 40 days of CPU time, requires 3 cores and 16GiB of RAM). We strongly discourage from running this inside a VM Run make transform-programs: To transform all the programs from termination to reachability for the verification runs in case, there is an error when running this command, we refer the user to the TransVer Section Run make verification-all to run the verification of the transformed programs to reachability for CPAchecker, UAUtomizer and Goblint, and the native verification using CPAchecker for termination. in case, there is an error when running this command, we recommend the user to apply the patches from the Known Issues Section Run make validation-all to validate the termination witnesses using MetaVal with all its possible backends, i.e., CPAchecker, and UAutomizer, and the validation using the two native validation approaches of CPAchecker. Run make generate-tables to generate html tables for each verifier presenting the results. These tables contain most of the results presented in the paper. (Optional) Generate the macros and csv used to generate the plots and tables in the paper: Run pip install -r data-analysis/requirements.txt. Run make analyze-results in order to export macros and csv files into the directory data-analysis/results. These were used to generate the plots and tables in the paper. Environment To run the artifact BenchExec, Python >= 3.8 and Podman are required. Inside a clean VM, please see the documentation of the respective tools for installation hints. A non-exhaustive list of required packages: * CPAchecker: Java 21 * UAutomizer: Java 21 * Goblint: libgmp-dev and libmpfr-dev We provide a setup script setup_vm.sh which installs all required dependencies inside the provided CAV 2026 Virtual Machine. NOTE: We assume that all the following commands are executed from inside the root directory of the artifact! NOTE: UAutomizer ships a custom version of Z3 which may not work on all systems, in particular it does not work inside the TACAS 26 VM (it works correctly inside CAV 2026 Virtual Machine). If you encounter issues with UAutomizer, please replace the shipped Z3 binary with a system-wide installed version of Z3. If you are using the TACAS 26 VM, this is already done for you. See the Known Issues section for more details. Using your system Z3 binary may also slow down UAutomizer significantly, so the results may differ from the ones presented in the paper. Experiments Setup Run source benchmark-utils/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 a single file, 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 ~30 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 40 days of CPU Time. Running the Experiments To run all experiments multiple targets need to be executed one after the other. Each of them encompass multiple targets for the different verifiers and validator backends. All experiments are run using BenchExec in order to ensure reliable benchmarks. The following targets need to be extecuted using make in this order: 1. transform-programs: Transforms all the chosen termination benchmarks using TransVer into reachability benchmarks. The produced benchmarks will follow the same directory structure and can be found in the folder benchmarks/sv-benchmarks-transformed. 2. verification-all: This executes the verifiers CPAchecker, UAutomizer and Goblint on the produced reachability tasks, in addition to the native termination analysis of CPAch