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

This artifact contains the tool HarnessForge and the infrastructure to create verification tasks from AWS C Common, Coreutils, and Intel TDX Module. We also include our generated task files. 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.1). 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.1 and Rancher Desktop 1.19.3 an AMD EPYC 7713 and 2 TB of RAM, running Ubuntu 24.04.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 18 GB of RAM and 5 CPU cores. The artifact requires less than 10 GB of disk space. Running the smoke tests takes 10-20 minutes. Reproducing the full task generation takes about 2 hours of run time on a Macbook Pro with M4 Pro and 24 GB of RAM. Reproducing all analysis runs on the created tasks before and after slicing takes about 40 days of run time. Overview The container contains two relevant directories: /data/harnessforge: A distribution of 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: Running the Docker container of this artifact (Section ‘Running the Artifact Image’ below) Smoke testing the artifact (Section ‘Smoke Test’ below) Task creation with HarnessForge and reproducing the results of our paper (Section ‘Full Task Creation’ below) For details about the direct use of HarnessForge in the container, see data/harnessforge/doc/tutorial/README.md for a short tutorial. For further information on using HarnessForge outside the container (reusable badge), please refer to data/harnessforge/README.md. Running the Artifact Image Follow the below steps to run the container. 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:fse26-demo. $ docker load -i HarnessForge-FSE-2026-Tool-Demo-container-image.tar Run a container from the loaded image: $ docker run -it --rm registry.gitlab.com/sosy-lab/research/data/harnessforge-automatic-extraction-of-verification-tasks/harnessforge:fse26-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 requested root@2e2f2c817e45:/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: cd /data/task-creation make smoke-test Expected terminal output: ## Running smoke test for AWS-C-Common ## /usr/bin/make -C aws-c-common smoke-test make[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.i make[1]: Leaving directory '/data/task-creation/tdx-module' Found 1 statistics files in /data/task-creation/aws-c-common/output_tasks/statistics Found 9 statistics files in /data/task-creation/coreutils/output_tasks/statistics Found 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: 17,048 LOC Average: 10,634.2 LOC LOC AFTER SLICING: Minimum: 292 LOC Maximum: 7,331 LOC Average: 3,948.8 LOC SLICING REDUCTION (%): Minimum: 57.0% Maximum: 90.6% Average: 62.9% ============================================================ Analyzed 20 verification tasks ============================================================ ============================================================ LATEX COMMANDS ============================================================ \newcommand{\numSmokeTestTaskCount}{20} \newcommand{\numSmokeTestMinimumRelevantFiles}{1} \newcommand{\numSmokeTestMaximumRelevantFiles}{20} \newcommand{\numSmokeTestAverageRelevantFiles}{11} \newcommand{\numSmokeTestMinimumLocBeforeSlicing}{3117} \newcommand{\numSmokeTestMaximumLocBeforeSlicing}{17048} \newcommand{\numSmokeTestAverageLocBeforeSlicing}{10634} \newcommand{\numSmokeTestMinimumLocAfterSlicing}{292} \newcommand{\numSmokeTestMaximumLocAfterSlicing}{7331} \newcommand{\numSmokeTestAverageLocAfterSlicing}{3949} \newcommand{\numSmokeTestMinimumReductionInPercent}{57.0} \newcommand{\numSmokeTestMaximumReductionInPercent}{90.6} \newcommand{\numSmokeTestAverageReductionInPercent}{62.9} ============================================================ ## Smoke tests completed successfully ## After running the smoke tests, you will find some generated tasks in 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 tasks mentioned 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): cd /data/task-creation make Expected output: Generating tasks for AWS-C-Common /usr/bin/make -C aws-c-common generate make[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.i make[1]: Leaving directory '/data/task-creation/tdx-module' Finished generating tasks for Intel TDX Module python3 scripts/slicing_stats.py --name AwsCCommon aws-c-common/output_tasks/statistics Found 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,991 LOC Maximum: 4,400 LOC Average: 4,213.9 LOC LOC AFTER SLICING: Minimum: 206 LOC Maximum: 317 LOC Average: 260.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}{2991} \newcommand{\numAwsCCommonMaximumLocBeforeSlicing}{4400} \newcommand{\numAwsCCommonAverageLocBeforeSlicing}{4214} \newcommand{\numAwsCCommonMinimumLocAfterSlicing}{206} \newcommand{\numAwsCCommonMaximumLocAfterSlicing}{317} \newcommand{\numAwsCCommonAverageLocAfterSlicing}{260} \newcommand{\numAwsCCommonMinimumReductionInPercent}{90.6} \newcommand{\numAwsCCommonMaximumReductionInPercent}{95.1} \newcommand{\numAwsCCommonAverageReductionInPercent}{93.8} ============================================================ python3 scripts/slicing_stats.py --name Coreutils coreutils/output_tasks/statistics Found 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,961 LOC Maximum: 7,320 LOC Average: 4,686.1 LOC LOC AFTER SLICING: Minimum: 600 LOC Maximum: 3,292 LOC Average: 1,159.5 LOC SLICING REDUCTION (%): Minimum: 55.0% Maximum: 86.2% Average: 75.3% ============================================================ Analyzed 48 verification tasks ============================================================ ============================================================ LATEX COMMANDS ============================================================ \newcommand{\numCoreutilsTaskCount}{48} \newcommand{\numCoreutilsMinimumRelevantFiles}{1} \newcommand{\numCoreutilsMaximumRelevantFiles}{4} \newcommand{\numCoreutilsAverageRelevantFiles}{3} \newcommand{\numCoreutilsMinimumLocBeforeSlicing}{3961} \newcommand{\numCoreutilsMaximumLocBeforeSlicing}{7320} \newcommand{\numCoreutilsAverageLocBeforeSlicing}{4686} \newcommand{\numCoreutilsMinimumLocAfterSlicing}{600} \newcommand{\numCoreutilsMaximumLocAfterSlicing}{3292} \newcommand{\numCoreutilsAverageLocAfterSlicing}{1159} \newcommand{\numCoreutilsMinimumReductionInPercent}{55.0} \newcommand{\numCoreutilsMaximumReductionInPercent}{86.2} \newcommand{\numCoreutilsAverageReductionInPercent}{75.3} ============================================================ python3 scripts/slicing_stats.py --name TDXModule tdx-module/output_tasks/statistics Found 836 statistics files in /data/task-creation/tdx-module/output_tasks/statistics Total: 836 statistics files ============================================================ SLICING STATISTICS REPORT ============================================================ NUMBER OF AGGREGATED FILES: Minimum: 9 Maximum: 28 Average: 14.8 LOC BEFORE SLICING: Minimum: 12,497 LOC Maximum: 26,574 LOC Average: 15,624.4 LOC LOC AFTER SLICING: Minimum: 2,952 LOC Maximum: 16,971 LOC Average: 6,246.6 LOC SLICING REDUCTION (%): Minimum: 36.1% Maximum: 76.5% Average: 60.0% ============================================================ Analyzed 836 verification tasks ============================================================ ============================================================ LATEX COMMANDS ============================================================ \newcommand{\numCoreutilsTaskCount}{836} \newcommand{\numCoreutilsMinimumRelevantFiles}{9} \newcommand{\numCoreutilsMaximumRelevantFiles}{28} \newcommand{\numCoreutilsAverageRelevantFiles}{15} \newcommand{\numCoreutilsMinimumLocBeforeSlicing}{12497} \newcommand{\numCoreutilsMaximumLocBeforeSlicing}{26574} \newcommand{\numCoreutilsAverageLocBeforeSlicing}{15624} \newcommand{\numCoreutilsMinimumLocAfterSlicing}{2952} \newcommand{\numCoreutilsMaximumLocAfterSlicing}{16971} \newcommand{\numCoreutilsAverageLocAfterSlicing}{6247} \newcommand{\numCoreutilsMinimumReductionInPercent}{36.1} \newcommand{\numCoreutilsMaximumReductionInPercent}{76.5} \newcommand{\numCoreutilsAverageReductionInPercent}{60.0} ============================================================ - 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 )