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: 多言語システムモデリングと検証のための合成的アプローチ

基本情報

論文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（プログラミング言語）
発表時期/会議: 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の加算はラップアラウンドが発生する可能性があります。
既存検証器の制限：ほとんどのプログラム検証器（CのためのCBMC、RustのためのKaniなど）は単一言語専用に設計されており、多言語システムを直接処理できません。
翻訳の複雑性：多言語システム全体を単一の検証言語に翻訳するには、すべての言語の完全な構文とセマンティクスをサポートする必要があり、現代の言語ではこれは実現不可能です。

研究の重要性

多言語システムの複雑性により、ソフトウェア欠陥のリスクが増加します。自動運転や航空宇宙などの安全関連分野では、テストなどの不完全な方法ではなく、形式的検証が提供する強力な保証が必要です。

既存方法の制限

単体翻訳方法：各言語に対して完全なコンパイラインフラストラクチャを開発する必要があります
セマンティクス保持の困難：ターゲット検証言語でソース言語のすべての言語固有の構成を忠実に捉えることは困難です
スケーラビリティの問題：生成される検証問題が過度に大きくなる可能性があります

コア貢献

多言語検証問題の形式化：多言語検証問題を初めて体系的に形式化し、複数の言語固有検証器を統合する合成的ソリューションを提案しました。
自動化契約合成：中間言語とCEGIS-CEGAR循環を使用した前置条件/後置条件契約の自動合成と細分化方法を提案し、構文ガイド合成と大規模言語モデルを合成予言として支持しています。
ツール実装：UCLID5に基づいてPolyVerツールを実装し、CとRustをサポートし、CBMCとKani検証器を通じて、LLMベースの合成予言が純粋な記号合成方法より優れていることを実証しました。
ケーススタディと評価：Lingua Franca調整言語の検証器を開発し、CとRustプロセスを含む多言語システムを検証し、以前の研究ではサポートされていなかったCコード片を検証しました。