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.

翻译：过去二十年间，针对C、C++和Java等特定语言的验证工具开发投入了大量研究与工程努力。许多现有验证方法本质上是与语言无关的，若能将其实现在其他编程和建模语言中复用，将极大促进技术转移。为解决此问题，我们提出SV-LIB——一种面向软件验证任务（包括程序、规约与验证凭证）的交换格式与中间语言。SV-LIB基于命令式编程语言的成熟概念，并采用SMT-LIB表示程序中的表达式与类型。由于多数验证工具已基于SMT求解器构建，该设计易于解析并集成至现有基础设施。此外，SV-LIB为正确与错误的SV-LIB程序定义了统一的凭证格式，同时提供凭证验证任务的规范方法。这使得开发独立的凭证验证器成为可能，并允许部分验证器复用为凭证验证工具。本文介绍SV-LIB格式的1.0版本，涵盖其设计目标、语法与非形式化语义。形式化语义及面向并发性的扩展将留待未来版本实现。