HarnessForge: Automated Extraction of Verification Tasks from Industry-Scale Software Projects
Journal
FSE Companion 2026 - Proceedings of the 34th ACM International Conference on the Foundations of Software Engineering
Start Page
202
End Page
206
ISBN
[9798400726361]
Date Issued
2026-07-05
Author(s)
Abstract
We present HarnessForge, a command-line tool to streamline the extraction of verification tasks from industry-scale software projects written in C. Industry-scale code consists of multiple source and header files with various build processes, complicating the creation of verification tasks and hindering the applicability of off-the-shelf software verifiers. HarnessForge handles this complexity for verification engineers and tools, allowing harnesses to be structured independently from the code under verification. It automatically derives build commands, assembles relevant source files, and performs static program slicing to remove irrelevant components. To demonstrate its applicability, we use HarnessForge to create a total of 949 verification tasks from three projects: AWS C Common, GNU Coreutils, and Intel TDX Module. All created tasks were used in SV-COMP 2026. A demo video is available at youtu.be/wHPEfQ3NBFQ.
Event(s)
ACM International Conference on the Foundations of Software Engineering, FSE 2026
Subjects
harnesses
industry-scale software
program slicing
software testing
software verification
verification tasks
Publisher
ACM
Type
conference paper