2025-11-24T00:55:25.034139

PolyVer: A Compositional Approach for Polyglot System Modeling and Verification

Chen, Lin, Godbole et al.

Several software systems are polyglot; that is, they comprise programs implemented in a combination of programming languages. Verifiers that directly run on mainstream programming languages are currently customized for single languages. Thus, to verify polyglot systems, one usually translates them into a common verification language or formalism on which the verifier runs. In this paper, we present an alternative approach, PolyVer, which employs abstraction, compositional reasoning, and synthesis to directly perform polyglot verification. PolyVer constructs a formal model of the original polyglot system as a transition system where the update functions associated with transitions are implemented in target languages such as C or Rust. To perform verification, PolyVer then connects a model checker for transition systems with language-specific verifiers (e.g., for C or Rust) using pre/post-condition contracts for the update functions. These contracts are automatically generated by synthesis oracles based on syntax-guided synthesis or large language models (LLMs), and checked by the language-specific verifiers. The contracts form abstractions of the update functions using which the model checker verifies the overall system-level property on the polyglot system model. PolyVer iterates between counterexample-guided abstraction-refinement (CEGAR) and counterexample-guided inductive synthesis (CEGIS) until the property is verified or a true system-level counterexample is found. We demonstrate the utility of PolyVer for verifying programs in the Lingua Franca polyglot language using the UCLID5 model checker connected with the CBMC and Kani verifiers for C and Rust respectively.

academic

PolyVer: A Compositional Approach for Polyglot System Modeling and Verification

基本信息

论文ID: 2503.03207
标题: PolyVer: A Compositional Approach for Polyglot System Modeling and Verification
作者: Pei-Wei Chen, Shaokai Lin, Adwait Godbole, Ramneet Singh, Elizabeth Polgreen, Edward A. Lee, Sanjit A. Seshia
分类: cs.PL (Programming Languages)
发表时间/会议: Formal Methods in Computer-Aided Design 2025
论文链接: https://arxiv.org/abs/2503.03207

摘要

多语言软件系统（polyglot systems）由多种编程语言实现的程序组合而成，但现有的程序验证器通常只针对单一语言定制。为验证多语言系统，通常需要将其翻译为通用验证语言或形式化表示。本文提出了PolyVer，一种采用抽象、组合推理和综合技术直接执行多语言验证的替代方法。PolyVer将多语言系统构建为转换系统的形式化模型，其中转换相关的更新函数用目标语言（如C或Rust）实现。为执行验证，PolyVer通过更新函数的前置/后置条件契约，连接转换系统的模型检查器与特定语言验证器。这些契约通过基于语法引导综合或大语言模型的综合预言自动生成，并由特定语言验证器检查。

研究背景与动机

问题定义

现代软件系统越来越多地采用多语言架构，如ROS2、Lingua Franca等框架允许开发者为不同组件选择最适合的编程语言。然而，这种灵活性带来了验证挑战：

语言语义差异：不同编程语言具有不同的语法和语义，如Rust的saturating_add函数在溢出时饱和到最大值，而C的加法可能发生环绕。
现有验证器局限：大多数程序验证器（如CBMC for C、Kani for Rust）专门针对单一语言设计，无法直接处理多语言系统。
翻译复杂性：将整个多语言系统翻译为单一验证语言需要支持所有语言的完整语法和语义，这对现代语言来说是禁止性的。

研究重要性

多语言系统的复杂性增加了软件缺陷的风险，而在安全关键领域（如自动驾驶、航空航天），需要形式化验证提供的强保证，而非仅仅依赖测试等不完整方法。

现有方法局限性

单体翻译方法：需要为每种语言开发完整的编译器基础设施
语义保持困难：难以在目标验证语言中忠实捕获源语言的所有语言特定构造
可扩展性问题：生成的验证问题可能变得过于庞大

核心贡献

多语言验证问题形式化：首次系统性地形式化了多语言验证问题，并提出集成多个特定语言验证器的组合解决方案。
自动化契约综合：提出了使用中间语言和CEGIS-CEGAR循环的前置/后置条件契约自动综合和细化方法，支持语法引导综合和大语言模型作为综合预言。
工具实现：基于UCLID5实现了PolyVer工具，支持C和Rust，通过CBMC和Kani验证器，证明了LLM-based综合预言优于纯符号综合方法。
案例研究与评估：开发了Lingua Franca协调语言的验证器，验证了包含C和Rust过程的多语言系统，以及之前工作无法支持的C语言片段。