Artifact for Tool Demonstration "HarnessForge: Automated Extraction of Verification Tasks from Industry-Scale Software Projects" (ASE 2025)

This artifact contains the tool HarnessForge and the infrastructureto create verification tasks from coreutils, AWS C common, and Intel TDX Module.We also include our generated task files. All of this is shipped in the container image 'HarnessForge-ASE-2025-Tool-Demo-container-image.tar' of this directory.To run the image: 1. Load the container image into your local registry: ```$ docker load -i HarnessForge-ASE-2025-Tool-Demo-container-image.tar``` 2. Run a container in this image: ```$ docker run -it --rm registry.gitlab.com/sosy-lab/research/data/harnessforge-automatic-extraction-of-verification-tasks/harnessforge:ase25-demo /bin/bash``` This opens a bash shell inside the container. ## Artifact Contents The container contains two relevant directories: - `/data/harnessforge`: A distribution of HarnessForge- `/data/task-creation`: Data for creating tasks from coreutils, AWS C common, and Intel TDX Module. This also contains our generated data. For more information on task creation, look at `/data/task-creation/README.md`. ## Paper Abstract We present HarnessForge, a command-line tool that automatesthe creation of verification tasks for industry-scale software projects written in C.Industry-scale code bases consist of multiple source and header files with a complex build process.HarnessForge removes the burden of handling this build process from software verifiersand enables verification engineers to structure harnesses independently from the code under verification.It automatically derives build commands, assembles relevant source files, and performs static program slicingto remove irrelevant components.To demonstrate its applicability, we apply HarnessForge to the code of AWS C Common, GNU Coreutils, and Intel’s TDX Module,creating a total of 444 verification tasks.Using the verification community’s task format enables users to apply nearly 100 verifiersand testers from the competitions on software verification (SV-COMP) and testing (Test-Comp).The Intel TDX Module tasks were used in SV-COMP 2025 to evaluate verifiers. A demo video is available at youtu.be/0WM9Lr8uV5o .