[Paper] SV-LIB 1.0：用于软件验证任务的标准交换格式

Source: arXiv - 2511.21509v1

Overview

在过去的二十年里，针对单一语言（如 C、C++ 和 Java）的验证工具研发投入了大量的研究与开发工作。许多使用的验证方法实际上是与语言无关的，如果能够让这些实现也用于其他编程和建模语言，将有助于技术的迁移。为了解决这一问题，我们提出了 SV‑LIB，一种用于软件验证任务（包括程序、规范和验证见证）的交换格式和中间语言。SV‑LIB 基于命令式编程语言的成熟概念，并使用 SMT‑LIB 来表示程序中使用的表达式和类型。这使得它易于解析并集成到现有基础设施中，因为许多验证工具已经基于 SMT 求解器。此外，SV‑LIB 为正确和错误的 SV‑LIB 程序定义了见证格式，并提供了指定见证验证任务的手段。这既可以实现独立的见证验证器，也可以将部分验证器复用为见证的验证器。本文展示了 SV‑LIB 格式的 1.0 版，包括其设计目标、语法以及非形式化语义。形式化语义及并发扩展计划在后续版本中实现。

Authors

• Dirk Beyer
• Gidon Ernst
• Martin Jonáš
• Marian Lingsch‑Rosenfeld

Categories

cs.PL, cs.SC, cs.SE

Paper Information

• arXiv ID: 2511.21509v1
• Categories: cs.PL, cs.SC, cs.SE
• Published: November 27, 2025
• PDF: Download PDF