FSE 2026
Sun 5 - Thu 9 July 2026 Montreal, Canada
Thu 9 Jul 2026 14:50 - 15:00 at MB 3.435 - Verification 2 Chair(s): Shiva Nejati

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 Jul

Displayed 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
20m
Talk
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
20m
Talk
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
10m
Talk
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
10m
Talk
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
10m
Talk
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
20m
Talk
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