HarnessForge: Automated Extraction of Verification Tasks from Industry-Scale Software Projects
Rattachement africain : de, us, tw. Niveau de preuve : code pays fourni par la source.
Le résumé fourni par la source
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.
Ce résumé expose les affirmations des auteurs. BNTIC ne l’interprète pas comme une validation indépendante des résultats.
Le contrôle bibliographique ouvert
DOI retrouvé dans Crossref DOI retrouvé ; titre concordant.
- Titre Crossref
- HarnessForge: Automated Extraction of Verification Tasks from Industry-Scale Software Projects
- Date Crossref
- 05/07/2026
- Éditeur
- ACM
- Type
- proceedings-article
Ce recoupement confirme des métadonnées liées au DOI. Il ne confirme ni la méthode ni les conclusions de l’étude, et il ne compte pas comme une seconde source scientifique indépendante.
Les institutions déclarées
Une affiliation ne permet pas de déduire la nationalité d’un auteur.