2026/01/01 by Tom Noël Goalard, Karoliine Holter, Simmo Saan +2 · 1 voice
Computer Science · #Formal Methods in Verification #Logic, programming, and type systems #Software Testing and Debugging Techniques
paper · doi:10.4230/lipics.ecoop.2026.8
openalex publication_date 2026/01/01 · openalex created_date 2026/06/26 · openalex updated_date 2026/07/29
Given an input program, sound static analyzers compute a list of potential runtime errors in it. However, measuring their precision and comparing their results remains challenging. In this work, we formalize a notion of transparent static analyzers that report the proof obligations they check, including both verified and unverified obligations. This transparent output enables a semantics-directed, fine-grained comparison and the combination of static analyzers. We introduce the Open Verification Dashboard (OVD), which provides a unified interface to aggregate the results of multiple static analyzers. By juxtaposing verified properties and outstanding warnings, OVD highlights coverage gaps, variabilities and inconsistencies across tools. We experimentally evaluate the benefits of OVD on benchmarks from the Competition on Software Verification (SV-COMP). This work paves the way for a static analysis standard for C runtime error reporting.