3 papers
cs.PL2025
SV-LIB 1.0: A Standard Exchange Format for Software-Verification Tasks
Dirk Beyer, Gidon Ernst, Martin Jonáš +1
In the past two decades, significant research and development effort went into the development of verification tools for individual languages, such asC, C++, and Java. Many of the…
cs.PL2025
A Modular Program-Transformation Framework for Reducing Specifications to Reachability
Dirk Beyer, Marek Jankola, Marian Lingsch-Rosenfeld +2
Software verification is a complex problem, and verification tools need significant tuning to achieve high performance. Due to this, many verifiers choose to specialize on reachabi…
cs.PL2025
Correctness Witnesses with Function Contracts
Matthias Heizmann, Dominik Klumpp, Marian Lingsch-Rosenfeld +1
Software verification witnesses are a common exchange format for software verification tools. They were developed to provide arguments supporting the verification result, allowing…