Artifact for the FASE 26 Paper: Testing in Formal Verification via Witness Generation (Empirical Evaluation)

Artifact for the FASE 26 Paper Testing in Formal Verification via Witness Generation (Empirical Evaluation) This artifact guides you through reproducing the plots and tables presented in the paper and through rerunning the experimental evaluation. The artifact is shipped as a VirtualBox VM. - The artifact is contained within a Ubuntu 24.04 VM. - We require at least 16 GB of Memory and 4 Cores Getting Started Username and Passworduser: test-to-witnesspassword: fase26 This artifact contains: analysis/ : Files concerning plots backup/ : A backup of the experiment data benchexec/ : The benchmarking tool benchmark-defs/ : Files defining benchmarks benchmark-sets/ : Files describing sets of tasks combinations/ : Code of the portfolio data/ : data from SV-COMP 25 expected/ : The expected plots Makefile results/ : Here are the generated witnesses from test-to-witness results-baseline/ : results of the baseline (just the verifier) for the portfolios results-portfolio/ : results of the portfolio experiments results-validate/ : results of the validation of generated witnesses results-verified/ : Data from Test-Comp 25 sv-benchmarks/ : The sv-benchmark tasks table-defs/ : Files defining how to create csv tables from the raw experiment data test-to-witness/ : The tool test-to-witness tool_info/ : Files telling benchexec how to run our tools validators/ : The validators used in the experiment If you are interested in just the tool Test-To-Witness you may navigate into the test-to-witness folder. There we include a README on how to use test-to-witness. Please note: We did not install a golang distribution in the VM, thus it is not possible to recompile test-to-witness. For the most up-to-date version we refer readers to our public gitlab: https://gitlab.com/sosy-lab/software/test-to-witness. This artifact document consists of the following steps: Downloading and installing the VM Recreating the plots and tables from the paper Running a subset of the experiments Running the full set of experiments For Getting Started we recommend doing Sections 1, 2 and 3.1 these should be able to be completed in less than 30min. Sections 2, 3 and 4 also serve as the Step-by-Step guide. 1. Download and Installation Instructions Download the artifact VM from Zenodo using the DOI provided with the paper. The download consists of a single VirtualBox appliance file with the extension .ova. Install Oracle VirtualBox (version 7 or newer is recommended) from the official website. Start VirtualBox and select File → Import Appliance. Choose the downloaded .ova file and follow the import wizard. You may adjust the VM settings during import; we require allocating at least 16 GB of RAM and 4 CPU cores. After the import finishes, select the VM from the list and click Start to launch it. Log in to the VM using the credentials: user: test-to-witness pw: fase26 2. Recreating the Plots and Tables of the Paper To recreate the plots, first open a terminal and change into the directory containing all data and scripts: cd $HOME/fase26 To generate all plots and tables used in the paper, run the following command (this takes approximately 1–2 minutes): make plots Expected Output: Copying data for plots... mkdir -p analysis/raw/ cp table-defs/portfolio-cpachecker.table.csv analysis/raw/ cp table-defs/portfolio-esbmc-kind.table.csv analysis/raw/ cp table-defs/portfolio-uautomizer.table.csv analysis/raw/ cp table-defs/portfolio-symbiotic.table.csv analysis/raw/ cp table-defs/portfolio-bubaak.table.csv analysis/raw/ cp table-defs/portfolio-cpv.table.csv analysis/raw/ cp data/reach_safety.table.csv analysis/raw/ cp results-verified/META_Cover-Error.table.csv analysis/raw/ cp table-defs/creation.table.csv analysis/raw/ cp table-defs/validation.table.csv analysis/raw/ Copied data successfully. Creating plots... cd analysis && python3 plot.py RQ1: Converted tasks (done): 10897 < 1.0s: 10490/10897 (96.27%) < 0.2s: 8069/10897 (74.05%) Created plots successfully. Plots are in the analysis/final_plots/ directory The generated plots are located in analysis/final_plots/.For convenience, we also provide the expected plots and tables in the directory expected/ so that you can directly compare results. 3. Running a Subset of the Experiments Because the full experiments are time-consuming, we provide a smoke-test mode that executes a small but representative subset of the experiments. There are three experiments in the paper: Creating witnesses from test suites Validating the generated witnesses Running parallel verifier–test-generator portfolios Backup of Results The experiments will write to the same files that the original experiments conducted by the authors wrote to. The benchmarking utility benchexec will terminate with an error if one of the old experiemt files is still present. In the following steps, we manually move result directories to make way for the new set of experiments about to be run. An additional backup of all original results is stored in backups/backup.tar.gz. It may be restored with make restore-experiment-data 3.1 RQ1: Creating Witnesses from Test Suites To generate witnesses from test cases, execute: cd $HOME/fase26 mv results results.bak make small-witnesses-from-testsuites Expected Output: PYTHONPATH=tool_info benchexec/bin/benchexec --read-only-dir=/ --hidden-dir /tmp --overlay-dir=/home --no-compress-results -o results/ --tool-directory test-to-witness --startTime '2025-10-16 10:29:27' benchmark-defs/small/test2witness.xml 2026-01-08 14:09:59 - WARNING - No propertyfile specified. Score computation will ignore the results. 2026-01-08 14:09:59 - INFO - Unable to find pqos_wrapper, please install it for cache allocation and monitoring if your CPU supports Intel RDT (cf. https://gitlab.com/sosy-lab/software/pqos-wrapper). executing run set 'esbmc-incr-coverage-error-call-confirmed.esbmc-incr-test-suites' (1 file) 14:09:59 06_fuzzle_50x50_0-cycle.yml done 2.30 2.67 executing run set 'fusebmc-coverage-error-call-confirmed.fusebmc-test-suites' (1 file) 14:10:02 array_ptr_single_elem_init-2.yml done 5.64 3.54 executing run set 'hybridtiger-coverage-error-call-confirmed.hybridtiger-test-suites' (1 file) 14:10:06 btor2c-lazyMod.driving_phils.3.prop1-func-interl.yml done 1.33 1.72 executing run set 'kleef-coverage-error-call-confirmed.kleef-test-suites' (1 file) 14:10:08 s4liff.yml done 0.26 0.49 executing run set 'owic-coverage-error-call-confirmed.owic-test-suites' (1 file) 14:10:08 elevator_spec3_product23.cil.yml done 0.33 0.57 executing run set 'tracerx-wp-coverage-error-call-confirmed.tracerx-wp-test-suites' (1 file) 14:10:09 list-2.yml done 175.25 167.49 executing run set 'utestgen-coverage-error-call-confirmed.utestgen-test-suites' (1 file) 14:12:57 rangesum.yml done 0.26 0.44 executing run set 'wasp-c-coverage-error-call-confirmed.wasp-c-test-suites' (1 file) 14:12:58 brs5f.yml done 0.21 0.70 Statistics: 8 Files correct: 0 correct true: 0 correct false: 0 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 0 In order to get HTML and CSV tables, run benchexec/bin/table-generator results/test2witness.2025-10-16_10-29-27.results.esbmc-incr-coverage-error-call-confirmed.esbmc-incr-test-suites.xml results/test2witness.2025-10-16_10-29-27.results.fusebmc-coverage-error-call-confirmed.fusebmc-test-suites.xml results/test2witness.2025-10-16_10-29-27.results.hybridtiger-coverage-error-call-confirmed.hybridtiger-test-suites.xml results/test2witness.2025-10-16_10-29-27.results.kleef-coverage-error-call-confirmed.kleef-test-suites.xml results/test2witness.2025-10-16_10-29-27.results.owic-coverage-error-call-confirmed.owic-test-suites.xml results/test2witness.2025-10-16_10-29-27.results.tracerx-wp-coverage-error-call-confirmed.tracerx-wp-test-suites.xml results/test2witness.2025-10-16_10-29-27.results.utestgen-coverage-error-call-confirmed.utestgen-test-suites.xml results/test2witness.2025-10-16_10-29-27.results.wasp-c-coverage-error-call-confirmed.wasp-c-test-suites.xml This command generates witnesses from test cases produced by 8 different test case generators and representing the different runtimes a conversion can take on. We recreate the creation.table.csv used by the plot script with our newly created data: make -B table-defs/creation.table.csv Expected Output: Generating creation.table.csv... benchexec/bin/table-generator -x table-defs/creation.xml -f csv --no-diff -o table-defs/ INFO: Reading table definition from 'table-defs/creation.xml'... WARNING: No file matches 'table-defs/../results/test2witness.2025-10-16_10-29-27.results.cetfuzz-coverage-error-call-confirmed.cetfuzz-test-suites.xml.bz2'. INFO: table-defs/../results/test2witness.2025-10-16_10-29-27.results.esbmc-incr-coverage-error-call-confirmed.esbmc-incr-test-suites.xml.bz2 WARNING: No file matches 'table-defs/../results/test2witness.2025-10-16_10-29-27.results.esbmc-kind-coverage-error-call-confirmed.esbmc-kind-test-suites.xml.bz2'. WARNING: No file matches 'table-defs/../results/test2witness.2025-10-16_10-29-27.results.fdse-coverage-error-call-confirmed.fdse-test-suites.xml.bz2'. WARNING: No file matches 'table-defs/../results/test2witness.2025-10-16_10-29-27.results.fizzer-coverage-error-call-confirmed.fizzer-test-suites.xml.bz2'. INFO: table-defs/../results/test2witness.2025-10-16_10-29-27.results.fusebmc-coverage-error-call-confirmed.fusebmc-test-suites.xml.bz2 WARNING: No file matches 'table-defs/../results/test2witness.2025-10-16_10-29-27.results.fu