一句话：HarnessForge 自动从工业级 C 项目提取验证任务，简化 harness 构建并生成 949 个 SV-COMP 任务。
工业级 C 软件项目通常包含多个源文件与头文件，并采用多种构建流程，这使得为现成软件验证器创建验证任务十分困难。HarnessForge 是一个命令行工具，旨在简化从这类项目中提取验证任务的过程：它允许验证 harness 独立于待验证代码进行结构化，自动推导构建命令、组装相关源文件，并通过静态程序切片移除无关组件。作者使用 HarnessForge 从 AWS C Common、GNU Coreutils 和 Intel TDX Module 三个项目中创建了共 949 个验证任务，这些任务全部用于 SV-COMP 2026，展示了工具在工业规模代码上的适用性。
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.
@inproceedings{BeyerCHLL26,
title = {HarnessForge: Automated Extraction of Verification Tasks from Industry-Scale Software Projects},
author = {Dirk Beyer and Po-Chun Chien and Bo-Yuan Huang and Nian-Ze Lee and Thomas Lemberger},
booktitle = {FSE},
year = {2026},
doi = {10.1145/3803437.3806420}
}