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

This artifact contains the tool HarnessForge and the infrastructureto create verification tasks from AWS C common, coreutils, and Intel TDX Module.We also include our generated task files. All of this is shipped in the container image 'HarnessForge-TACAS-2026-Tool-Demo-container-image.tar' of this artifact. ## Paper Abstract We present HarnessForge, a command-line tool that automatesthe creation of verification tasks for industry-scale software projectswritten in C. Industry-scale code consists of multiple source and headerfiles with various build processes. HarnessForge handles these buildprocesses for software verifiers and enables verification engineers to structureharnesses independently from the code under verification. It automaticallyderives build commands, assembles relevant source files, and performsstatic program slicing to remove irrelevant components. To demonstrateits applicability, we apply HarnessForge to the code of AWS C Common,GNU Coreutils, and Intel’s TDX Module, creating a total of 512 verification tasks.The Intel TDX Module tasks were used in SV-COMP 2025and additional tasks are submitted to SV-COMP 2026. ### Container Image and Test Environment The artifact is a linux/amd64 container image, built with Docker version 28.2.2, build e6534b4.The container can be run on arm64 architecture through emulation(tested with Rancher Desktop 1.19.3 on an M4 Macbook with macOS 26.0). The container image is based on Ubuntu 22.04. The artifact was tested on: - an M4 Pro and 24 GB of RAM, running macOS 26.0 and Rancher Desktop 1.19.3- an AMD EPYC 7713 and 2 TB of RAM, running Ubuntu 24.0.4.3 LTS and podman 4.9.3 ### Hardware Requirements and Time Estimates To run the artifact and reproduce the results of our paper,we recommend a machine with at least 16 GB of RAM and 4 CPU cores.The artifact requires less than 10 GB of disk space. Running the smoke tests takes 10-20 minutes.Reproducing the full results of our paper takes about 2 hourson a Macbook Pro with M4 Pro and 24 GB of RAM. ### Overview The container contains two relevant directories: - `/data/harnessforge`: A distribution of [HarnessForge](https://gitlab.com/sosy-lab/software/harnessforge)- `/data/task-creation`: Data for creating tasks from AWS C Common, Coreutils, and Intel TDX Module. This also contains our generated data. This README contains information on: 1. Running the Docker container of this artifact (Section 'Running the Artifact Image' below)2. Smoke testing the artifact (Section 'Smoke Test' below)3. Task creation with HarnessForge and reproducing the results of our paper (Section 'Full Task Creation' below)4. For details about the direct use of HarnessForge in the container, see `data/harnessforge/doc/tutorial/README.md` for a short tutorial.5. For further information on using HarnessForge outside the container (reusable badge), please refer to `data/harnessforge/README.md`. ## Running the Artifact Image **After you downloaded the image** from [this link](https://doi.org/10.5281/zenodo.17376254),follow the below steps to run the container. 1. Load the container image into your local registry with the below command. This loads the image with name `registry.gitlab.com/sosy-lab/research/data/harnessforge-automatic-extraction-of-verification-tasks/harnessforge:tacas26-demo`. ```shell$ docker load -i HarnessForge-TACAS-2026-Tool-Demo-container-image.tar``` 2. Run a container from the loaded image: ```shell$ docker run -it --rm registry.gitlab.com/sosy-lab/research/data/harnessforge-automatic-extraction-of-verification-tasks/harnessforge:tacas26-demo /bin/bash``` This creates the container and opens a bash shell inside. _Expected output_: ```WARNING: The requested image's platform (linux/amd64) does not match the detected host platform (linux/arm64/v8) and no specific platform was requestedroot@27dd4f748b1b:/data#``` The warning is expected if you are running the container from a host that is not an amd64 architecture. ## Smoke Tests For smoke tests, we check that the task-creation pipeline for all three original projects works.This takes 10-20 minutes after starting the container. To run the smoke tests: ```shellcd /data/task-creationmake smoke-test``` _Expected terminal output_: ```## Running smoke test for AWS-C-Common ##/usr/bin/make -C aws-c-common smoke-testmake[1]: Entering directory '/data/task-creation/aws-c-common'cd aws-c-common-project \&& rm -rf formal && mkdir -p formal \&& cp -r ../formal/* formal/ \&& cp formal/project-config.yaml ./ \&& for taskconfig in formal/configs/aws_add_size_checked.yml; do harnessforge create-task "$taskconfig" 2>/tmp/hf-$(basename $taskconfig).log; done \&& mkdir -p ../output_tasks \&& cp -r output_tasks/* ../output_tasks/🔧 Creating task file for aws_add_size_checked_harness * Computing relevant sources * Assembling single-file verification task * Slicing verification task🧰 Task file written to output_tasks/aws_add_size_checked_harness.i # .. snip similar output for more tasks from coreutils and tdx-module .. 🧰 Task file written to output_tasks/tdg_mr_report__unconstrained__cover_exit_success.i🔧 Creating task file for tdg_mr_report__unconstrained__cover_exit_unsuccess * Computing relevant sources * Assembling single-file verification task * Slicing verification task🧰 Task file written to output_tasks/tdg_mr_report__unconstrained__cover_exit_unsuccess.imake[1]: Leaving directory '/data/task-creation/tdx-module'Found 1 statistics files in /data/task-creation/aws-c-common/output_tasks/statisticsFound 9 statistics files in /data/task-creation/coreutils/output_tasks/statisticsFound 10 statistics files in /data/task-creation/tdx-module/output_tasks/statistics Total: 20 statistics files ============================================================SLICING STATISTICS REPORT============================================================ NUMBER OF AGGREGATED FILES: Minimum: 1 Maximum: 20 Average: 11.2 LOC BEFORE SLICING: Minimum: 3,117 LOC Maximum: 18,002 LOC Average: 11,116.6 LOC LOC AFTER SLICING: Minimum: 292 LOC Maximum: 8,130 LOC Average: 4,349.4 LOC SLICING REDUCTION (%): Minimum: 54.8% Maximum: 90.6% Average: 60.9% ============================================================Analyzed 20 verification tasks============================================================ ============================================================LATEX COMMANDS============================================================ \newcommand{\numSmokeTestTaskCount}{20}\newcommand{\numSmokeTestMinimumRelevantFiles}{1}\newcommand{\numSmokeTestMaximumRelevantFiles}{20}\newcommand{\numSmokeTestAverageRelevantFiles}{11}\newcommand{\numSmokeTestMinimumLocBeforeSlicing}{3117}\newcommand{\numSmokeTestMaximumLocBeforeSlicing}{18002}\newcommand{\numSmokeTestAverageLocBeforeSlicing}{11117}\newcommand{\numSmokeTestMinimumLocAfterSlicing}{292}\newcommand{\numSmokeTestMaximumLocAfterSlicing}{8130}\newcommand{\numSmokeTestAverageLocAfterSlicing}{4349}\newcommand{\numSmokeTestMinimumReductionInPercent}{54.8}\newcommand{\numSmokeTestMaximumReductionInPercent}{90.6}\newcommand{\numSmokeTestAverageReductionInPercent}{60.9} ============================================================## Smoke tests completed successfully ##``` After running the smoke tests, you will find some generated tasksin the following three directories: - `/data/task-creation/aws-c-common/output_tasks/` (1 task)- `/data/task-creation/coreutils/output_tasks/` (9 tasks)- `/data/task-creation/tdx-module/output_tasks/` (10 tasks) Each task consists of three files: `.i`, `.c`, and `.yml`.Please check that they have been created successfully. ## Full Task Creation In the artifact container image, directory `/data/task-creation`contains the data for creating the benchmark tasksmentioned in our paper: - For AWS C Common: Directory `/data/task-creation/aws-c-common`- For Coreutils: Directory `/data/task-creation/coreutils`- For Intel TDX Module: Directory `/data/task-creation/tdx-module` Each of these directories contain: - a `Makefile`- a `formal` directory that contains harnessforge configuration and overrides, and- the original project, with the formal directory and `project-configuration.yaml` copied into it. ### Commands To reproduce all benchmark tasks and afterwards print the slicing statistics, run (this takes about 2 hours on a Macbook Pro with M4 Pro): ```shellcd /data/task-creationmake``` Expected output: ```Generating tasks for AWS-C-Common/usr/bin/make -C aws-c-common generatemake[1]: Entering directory '/d/data/task-creation/aws-c-common'cd aws-c-common-project \&& rm -rf formal && mkdir -p formal \&& cp -r ../formal/* formal/ \&& cp formal/project-config.yaml ./ \&& for taskconfig in formal/configs/*.yml; do harnessforge create-task "$taskconfig" 2>/tmp/hf-$(basename $taskconfig).log; done \&& mkdir -p ../output_tasks \&& cp -r output_tasks/* ../output_tasks/🔧 Creating task file for aws_add_size_checked_harness * Computing relevant sources * Assembling single-file verification task * Slicing verification task🧰 Task file written to output_tasks/aws_add_size_checked_harness.i🔧 Creating task file for aws_add_size_saturating_harness# .. snip similar output for more tasks from coreutils and tdx-module .. 🧰 Task file written to output_tasks/tdh_vp_enter__invalid_state_pamt_metadata__cover_proof.i🔧 Creating task file for tdh_vp_enter__unconstrained__cover_exit_unsuccess * Computing relevant sources * Assembling single-file verification task * Slicing verification task🧰 Task file written to output_tasks/tdh_vp_enter__unconstrained__cover_exit_unsuccess.imake[1]: Leaving directory '/data/task-creation/tdx-module'Finished generating tasks for Intel TDX Modulepython3 scripts/slicing_stats.py --name AwsCCommon aws-c-common/output_tasks/statisticsFound 20 statistics files in /data/task-creation/aws-c-common/output_tasks/statistics Total: 20 statistics files ============================================================SLICING STATISTICS REPORT============================================================ NUMBER OF AGGREGATED FILES: Minimum: 1 Maximum: 4 Average: 3.5 LOC BEFORE SLICING: Minimum: 2,984 LOC Maximum: 4,393 LOC Average: 4,206.9 LOC LOC AFTER SLICING: Minimum: 205 LOC Maximum: 316 LOC Average: 259.2 LOC SLICING REDUCTION (%): Minimum: 90.6% Maximum: 95.1% Average: 93.8% ============================================================Analyzed 20 verification tasks============================================================ ============================================================LATEX COMMANDS============================================================ \newcommand{\numAwsCCommonTaskCount}{20}\newcommand{\numAwsCCommonMinimumRelevantFiles}{1}\newcommand{\numAwsCCommonMaximumRelevantFiles}{4}\newcommand{\numAwsCCommonAverageRelevantFiles}{4}\newcommand{\numAwsCCommonMinimumLocBeforeSlicing}{2984}\newcommand{\numAwsCCommonMaximumLocBeforeSlicing}{4393}\newcommand{\numAwsCCommonAverageLocBeforeSlicing}{4207}\newcommand{\numAwsCCommonMinimumLocAfterSlicing}{205}\newcommand{\numAwsCCommonMaximumLocAfterSlicing}{316}\newcommand{\numAwsCCommonAverageLocAfterSlicing}{259}\newcommand{\numAwsCCommonMinimumReductionInPercent}{90.6}\newcommand{\numAwsCCommonMaximumReductionInPercent}{95.1}\newcommand{\numAwsCCommonAverageReductionInPercent}{93.8} ============================================================python3 scripts/slicing_stats.py --name Coreutils coreutils/output_tasks/statisticsFound 48 statistics files in /data/task-creation/coreutils/output_tasks/statistics Total: 48 statistics files ============================================================SLICING STATISTICS REPORT============================================================ NUMBER OF AGGREGATED FILES: Minimum: 1 Maximum: 4 Average: 2.9 LOC BEFORE SLICING: Minimum: 3,913 LOC Maximum: 7,272 LOC Average: 4,638.1 LOC LOC AFTER SLICING: Minimum: 593 LOC Maximum: 3,285 LOC Average: 1,152.5 LOC SLICING REDUCTION (%): Minimum: 54.8% Maximum: 86.2% Average: 75.2% ============================================================Analyzed 48 verification tasks============================================================ ============================================================LATEX COMMANDS============================================================ \newcommand{\numCoreutilsTaskCount}{48}\newcommand{\numCoreutilsMinimumRelevantFiles}{1}\newcommand{\numCoreutilsMaximumRelevantFiles}{4}\newcommand{\numCoreutilsAverageRelevantFiles}{3}\newcommand{\numCoreutilsMinimumLocBeforeSlicing}{3913}\newcommand{\numCoreutilsMaximumLocBeforeSlicing}{7272}\newcommand{\numCoreutilsAverageLocBeforeSlicing}{4638}\newcommand{\numCoreutilsMinimumLocAfterSlicing}{593}\newcommand{\numCoreutilsMaximumLocAfterSlicing}{3285}\newcommand{\numCoreutilsAverageLocAfterSlicing}{1152}\newcommand{\numCoreutilsMinimumReductionInPercent}{54.8}\newcommand{\numCoreutilsMaximumReductionInPercent}{86.2}\newcommand{\numCoreutilsAverageReductionInPercent}{75.2} ============================================================python3 scripts/slicing_stats.py --name TDXModule tdx-module/output_tasks/statisticsFound 444 statistics files in /data/task-creation/tdx-module/output_tasks/statistics Total: 444 statistics files ============================================================SLICING STATISTICS REPORT============================================================ NUMBER OF AGGREGATED FILES: Minimum: 9 Maximum: 28 Average: 14.6 LOC BEFORE SLICING: Minimum: 13,431 LOC Maximum: 26,482 LOC Average: 15,979.5 LOC LOC AFTER SLICING: Minimum: 3,445 LOC Maximum: 16,786 LOC Average: 6,494.5 LOC SLICING REDUCTION (%): Minimum: 36.6% Maximum: 74.4% Average: 59.4% ============================================================Analyzed 444 verification tasks============================================================ ============================================================LATEX COMMANDS============================================================ \newcommand{\numTDXModuleTaskCount}{444}\newcommand{\numTDXModuleMinimumRelevantFiles}{9}\newcommand{\numTDXModuleMaximumRelevantFiles}{28}\newcommand{\numTDXModuleAverageRelevantFiles}{15}\newcommand{\numTDXModuleMinimumLocBeforeSlicing}{13431}\newcommand{\numTDXModuleMaximumLocBeforeSlicing}{26482}\newcommand{\numTDXModuleAverageLocBeforeSlicing}{15980}\newcommand{\numTDXModuleMinimumLocAfterSlicing}{3445}\newcommand{\numTDXModuleMaximumLocAfterSlicing}{16786}\newcommand{\numTDXModuleAverageLocAfterSlicing}{6494}\newcommand{\numTDXModuleMinimumReductionInPercent}{36.6}\newcommand{\numTDXModuleMaximumReductionInPercent}{74.4}\newcommand{\numTDXModuleAverageReductionInPercent}{59.4} ============================================================- Tasks created from AWS C Commons are available at aws-c-common/output_tasks (The tasks shipped with this artifact are available for comparison at aws-c-common/created-tasks )- Tasks created from coreutils are available at coreutils/output_tasks (The tasks shipped with this artifact are available for comparison at coreutils/created-tasks )- Tasks created from tdx-module are available at tdx-module/output_tasks (The tasks shipped with this artifact are available for comparison at tdx-module/created-tasks )```