HarnessForge: Automated Extraction of Verification Tasks from Industry-Scale Software Projects
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.
Thu 9 JulDisplayed time zone: Eastern Time (US & Canada) change
14:00 - 15:30 | Verification 2Tool Demonstrations / Ideas, Visions and Reflections / Research Papers at MB 3.435 Chair(s): Shiva Nejati University of Ottawa | ||
14:00 20mTalk | Agentic Verification of Software Systems Research Papers Haoxin Tu National University of Singapore, Huan Zhao National University of Singapore, Yahui Song Standard Chartered Bank, Mehtab Zafar National University of Singapore, Ruijie Meng CISPA Helmholtz Center for Information Security, Abhik Roychoudhury National University of Singapore Pre-print | ||
14:20 20mTalk | DiverFPS: Generating Diverse Solutions for Floating-Point SMT Formulas Research Papers Shuangyu Lyu Beihang University, Chuan Luo Beihang University, Ruizhi Shi Beihang University, Zhuo Su Beihang University, Chunming Hu Beihang University | ||
14:40 10mTalk | The Watermark Paradox: How Provenance Verification Paves the Road to Camouflaged Backdoors Ideas, Visions and Reflections Haoyi Zhang Xi’an Jiaotong-Liverpool University, Huaijin Ran Xi’an Jiaotong-Liverpool University, Kisub Kim DGIST, Xunzhu Tang University of Luxembourg DOI | ||
14:50 10mTalk | HarnessForge: Automated Extraction of Verification Tasks from Industry-Scale Software Projects Tool Demonstrations Dirk Beyer LMU Munich, Po-Chun Chien LMU Munich, Bo-Yuan Huang Intel, USA, Nian-Ze Lee National Taiwan University, Taiwan, Thomas Lemberger LMU Munich Pre-print Media Attached | ||
15:00 10mTalk | PyMOP: A Runtime Verification Tool for Python Tool Demonstrations Zhuohang Shen Cornell University, Mohammed S. Yaseen Independent Researcher, Kevin Guan Cornell University, Denini Silva Federal University of Pernambuco, Marcelo d'Amorim North Carolina State University, Owolabi Legunsen Cornell University | ||
15:10 20mTalk | Property Refinement in Linear Temporal Logic: Formal Semantics and Algorithms for Software Verification Research Papers Luca Brodo Hochschule Hamm-Lippstadt, Giuseppe Scalora Hamm-Lippstadt University of Applied Sciences, Stefan Henkler Hochschule Hamm-Lippstadt File Attached | ||