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.

翻译：许多软件系统是多语言的，即它们由多种编程语言组合实现的程序构成。当前直接运行于主流编程语言的验证器通常仅针对单一语言定制。因此，为验证多语言系统，通常需要将其转换为验证器可运行的通用验证语言或形式化模型。本文提出一种替代方案PolyVer，该方法通过抽象化、组合推理与综合技术直接执行多语言验证。PolyVer将原始多语言系统构建为形式化迁移系统模型，其中与迁移关联的更新函数以C或Rust等目标语言实现。为执行验证，PolyVer通过更新函数的前后置条件契约，将迁移系统模型检查器与特定语言验证器（如针对C或Rust的验证器）相连接。这些契约由基于语法引导综合或大语言模型的综合预言机自动生成，并由特定语言验证器进行检查。契约构成更新函数的抽象表示，模型检查器据此在多语言系统模型上验证整体系统级属性。PolyVer在反例引导的抽象精化与反例引导的归纳综合之间迭代执行，直至属性被验证或发现真实的系统级反例。我们通过将UCLID5模型检查器分别与C语言验证器CBMC和Rust语言验证器Kani相连接，演示了PolyVer在验证Lingua Franca多语言程序中的实用性。