SV-LIB 1.0: A Standard Exchange Format for Software-Verification Tasks

TL;DR

SV-LIB 1.0 introduces a standard exchange format for software verification tasks by extending SMT-LIB with imperative programming constructs, including global variables, procedures, and both structured and unstructured control flow. It enables verification tasks to be shared across tools via a unified syntax for programs, specifications, and witnesses, and supports a formal witness format for correctness and violation evidence. The design emphasizes interoperability between automatic and deductive verification communities, incremental solver interaction, and trace-based validation, with well-defined concepts for task construction, validation, and tool integration. By decoupling frontends from backends and providing tooling such as PySvLib, ANTLR grammars, and CPAchecker integration, SV-LIB aims to accelerate technology transfer and cross-community collaboration in software verification.

Abstract

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 used verification approaches are in fact language-agnostic and it would be beneficial for the technology transfer to allow for using the implementations also for other programming and modeling languages. To address the problem, we propose SV-LIB, an exchange format and intermediate language for software-verification tasks, including programs, specifications, and verification witnesses. SV-LIBis based on well-known concepts from imperative programming languages and uses SMT-LIB to represent expressions and sorts used in the program. This makes it easy to parse and to build into existing infrastructure, since many verification tools are based on SMT solvers already. Furthermore, SV-LIBdefines a witness format for both correct and incorrect SV-LIB programs, together with means for specifying witness-validation tasks. This makes it possible both to implement independent witness validators and to reuse some verifiers also as validators for witnesses. This paper presents version 1.0 of the SV-LIBformat, including its design goals, the syntax, and informal semantics. Formal semantics and further extensions to concurrency are planned for future versions.

Figures (14)

• Figure 1: Possible transformations and use-cases for SV-LIB as an intermediate language
• Figure 2: Procedure add written in C
• Figure 3: Correct SV-LIB program that fulfills all its specifications (left) and a possible witness for it (right); scripts available at the https://gitlab.com/sosy-lab/benchmarking/sv-lib repo as https://gitlab.com/sosy-lab/benchmarking/sv-lib/-/blob/format-1.0/examples/core-verification/loop-add.svlib and https://gitlab.com/sosy-lab/benchmarking/sv-lib/-/blob/format-1.0/examples/core-validation/loop-add.svlib tasks
• Figure 4: Two parts of an SV-LIB script showing incremental solver interaction; the solver may choose to maintain a state across multiple verify-call commands to be more efficient; script available at the https://gitlab.com/sosy-lab/benchmarking/sv-lib repo as https://gitlab.com/sosy-lab/benchmarking/sv-lib/-/blob/format-1.0/examples/core-verification/loop-add-incremental.svlib
• Figure 5: Incorrect SV-LIB program violating a safety property (left) and a possible witness for it (right), which provides the initial values of the global constants x1 and y1 and claims that no further choices need to be resolved to follow the execution to a violation of the postcondition. Scripts available at the https://gitlab.com/sosy-lab/benchmarking/sv-lib repo as https://gitlab.com/sosy-lab/benchmarking/sv-lib/-/blob/format-1.0/examples/core-verification/loop-add-incorrect-ensures.svlib and https://gitlab.com/sosy-lab/benchmarking/sv-lib/-/blob/format-1.0/examples/core-validation/loop-add-incorrect-ensures.svlib tasks