Formal Method Final Report - Reproduction Package

# Reproduction Package ## Formal Methods (EE5122) Final report Artifact [10.5281/zenodo.20812690](https://doi.org/10.5281/zenodo.20812690) ### Abstract This artifact is a reproduction package for the Final report of the Formal Methods course of National Taiwan University. This package is archived on Zenodo with the DOI [10.5281/zenodo.20812690](https://doi.org/10.5281/zenodo.20812690). This artifact is mainly based on the reproduction package for the [article](https://dl.acm.org/doi/pdf/10.1145/3660797) "A Transferability Study of Interpolation-Based Hardware Model Checking to Software Verification", accepted at FSE 2024, with the DOI [10.5281/zenodo.11070973](https://doi.org/10.5281/zenodo.11070973). The artifact consists of source code, precompiled executables, and input data used in the evaluation and the experiment results. Specifically, it includes the source code and binaries of modified [CPV](https://gitlab.com/sosy-lab/software/cpv) programs , which implements the verification algorithms, the SV-COMP 2025 [benchmark suite](https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks) (at main branch in June 19th, 2026), the experimental data generated from the evaluation, and instructions to run the tools and experiments. This reproduction package works best with the [SoSy-Lab Virtual Machine](https://doi.org/10.5281/zenodo.8245829), which runs Ubuntu 22.04 LTS and has all the required dependencies installed. If you test this artifact with this VM, you will need to install some additional package, see [TL;DR](#TL;DR). Due to hardware resource and time limitation, we assign 1 CPU cores, 6 GB of memory, and 300 s of CPU time limit to each verification task. ### Contents This artifact contains the following items: - [`README.md`](README.md): this documentation - [`LICENSE.txt`](LICENSE.txt): license information of the artifact - [`doc/`](doc/): a directory containing the additional information of the artifact, including - [`INSTALL.md`](doc/INSTALL.md): installation guide for the software dependencies - [`STATUS.md`](doc/STATUS.md): the artifact badges we are applying for and the justifications - [`cpv/`](cpv/): a directory containing the [source code](https://gitlab.com/sosy-lab/software/CPV) - [`sv-benchmarks/`](sv-benchmarks/): a directory containing the SV-COMP 2025 [benchmark tasks](https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/tree/main) used in our evaluation - [`data/`](data/): a directory containing the raw and processed data produced from our full evaluation (used in the report, under [`exp-results/`](data/exp-results/) and ['exp-time-results/'](data/exp-time-results/)) - [`src/`](src/): a directory for source codes. - [`bench-defs/`](bench-defs/): a directory containing the benchmark and table definitions of the experiments (used by [BenchExec](https://github.com/sosy-lab/benchexec), a framework for reliable benchmarking) - [`Makefile`](Makefile): a file that assembles commands for running experiments and processing data This README file will guide you through the following steps: - [Set up evaluation environment](#set-up-evaluation-environment) - [Execute CPV on example programs](#execute-CPV) - [Reproduce experiments in the paper](#conduct-experiments) - Compare _ABC_, _AVR_, and _rIC3_ against each other on software verification tasks. - [Interpret the experimental results](#view-the-experimental-results)