DOI: 10.5281/zenodo.18348148
title: Container for Tool Demonstration "HarnessForge: Automated Extraction of Verification Tasks from Industry-Scale Software Projects" (FSE 2026)

description: 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 )