論文の概要: ConVer: Using Contracts and Loop Invariant Synthesis for Scalable Formal Software Verification
- arxiv url: http://arxiv.org/abs/2605.27051v1
- Date: Tue, 26 May 2026 14:04:40 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-05-27 17:51:42.209119
- Title: ConVer: Using Contracts and Loop Invariant Synthesis for Scalable Formal Software Verification
- Title（参考訳）: ConVer: スケーラブルな形式ソフトウェア検証のための契約とループ不変合成
- Authors: Muhammad A. A. Pirzada, Weiqi Wang, Yiannis Charalambous, Konstantin Korovin, Lucas C. Cordeiro,
- Abstract要約: トップダウンのコンポジション検証ツールであるConVerを紹介します。
トップレベルのアサーションを持つCプログラムの場合、ConVerは検証トップダウンを分解する。
ConVerを4つのベンチマークスイートで評価し、難易度を高め、他のSOTA(State-of-the-art)ツールと比較した。
- 参考スコア（独自算出の注目度）: 9.620677246257232
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Formal verification of large C programs is impeded by state-space explosion: Bounded Model Checking (BMC) tools must encode the entire state space up to the predetermined bound by unrolling all nested constructs. We present ConVer, a top-down compositional verification tool. Given a C program with a top-level assertion, ConVer decomposes verification top-down: it uses a large language model (LLM) to synthesise function contracts from the system property, then alternates system-level and function-level checks in a CEGAR-CEGIS loop, refining contracts whenever a check fails via SMART ICE learning. We evaluate ConVer on four benchmark suites of increasing difficulty and against other state-of-the-art (SOTA) tools. On the Frama-C benchmark of 45 simple C programs, ConVer achieves 82-96% verification success across three LLM backends, with 93-95% of converged programs requiring only a single CEGAR-CEGIS iteration. On the X.509 parser benchmark (6~programs) and LF2C-Simple suite (17 programs), ConVer achieves 33-50% and 82-88% success respectively. On the VerifyThis suite of 11 recursive and loop-intensive programs, the Pre-Abstraction strategy achieves 55-64% success. In addition, we present ESBMC-LF a preprocessor tool that converts LF models to C while preserving the properties of the LF files, enabling ConVer to verify them. We transpile the LF Verifier Benchmarks using ESBMC-LF to C; we denote those LF-Hard. We show that ConVer successfully verifies 67% of LF-Hard benchmarks overall.
- Abstract（参考訳）: 境界モデルチェック(BMC)ツールは、すべてのネストされた構成物をアンロールすることで、所定の境界まで状態空間全体をエンコードしなければならない。
トップダウンのコンポジション検証ツールであるConVerを紹介します。
システムプロパティから関数コントラクトを合成するために大きな言語モデル(LLM)を使用し、CEGAR-CEGISループでシステムレベルと関数レベルのチェックを交換し、チェックがSMART ICE学習で失敗するたびにコントラクトを精査する。
ConVerを4つのベンチマークスイートで評価し、難易度を高め、他のSOTA(State-of-the-art)ツールと比較した。
45の単純なCプログラムのFrama-Cベンチマークでは、ConVerは3つのLLMバックエンドで82-96%の検証成功を達成し、93-95%の収束プログラムは1回のCEGAR-CEGISイテレーションしか必要としない。
X.509パーサベンチマーク(プログラム6～プログラム)とLF2C-Simpleスイート(17プログラム)では、ConVerはそれぞれ33-50%と82-88%の成功を収めている。
再帰的かつループ集約的な11のプログラムからなるVerifyThisスイートでは、Pre-Abstraction戦略が55-64%の成功を達成している。
さらに,提案する ESBMC-LF は,LF モデルを C に変換しながら LF ファイルのプロパティを保存し,ConVer が検証可能なプリプロセッサツールである。
我々は、ESBMC-LFを使ってLF検証ベンチマークをCに変換する。
ConVerはLF-Hardベンチマーク全体の67%の検証に成功していることを示す。
関連論文リスト
- CODESTRUCT: Code Agents over Structured Action Spaces [14.039220358416104]
LLMベースのコードエージェントは、リポジトリを非構造化テキストとして扱い、脆いマッチング文字列を通じて編集を適用する。
我々は、エージェントがテキストスパンではなく名前付きASTエンティティを操作するような構造化されたアクション空間として再フレーミングを提案する。
私たちのフレームワークであるCODESTRUCTは、完全な構文単位を取得するためのreadCodeと、構文検証された変換をセマンティックプログラム要素に適用するためのEditCodeを提供します。
論文 参考訳（メタデータ） (2026-04-07T03:58:10Z) - SPARC: Scenario Planning and Reasoning for Automated C Unit Test Generation [1.0010193170880752]
本稿では,高レベルのプログラム意図とポインタ演算と手動メモリ管理の厳密な構文制約とのギャップを埋める,ニューロシンボリックなシナリオベースのフレームワークを提案する。
我々は、59の現実世界およびアルゴリズムの被験者で評価し、バニラプロンプト生成ベースラインを31.36%、分岐カバレッジ26.01%、突然変異スコア20.78%で上回り、シンボリック実行ツールKLEEに適合または超えている。
論文 参考訳（メタデータ） (2026-02-18T18:09:03Z) - AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithms [54.99368693313797]
既存のベンチマークでは、個々の言語/ツールのみをテストするため、パフォーマンス番号は直接比較できない。
このギャップに対処するAlgoVeriは、Dafny、Verus、Leanで77ドルの古典的アルゴリズムのベリコーディングを評価するベンチマークです。
論文 参考訳（メタデータ） (2026-02-10T06:58:26Z) - Synthesizing File-Level Data for Unit Test Generation with Chain-of-Thoughts via Self-Debugging [40.29934051200609]
本稿では,高品質なUTトレーニングを実現するための新しいデータ蒸留手法を提案する。
このパイプラインをオープンソースプロジェクトの大規模なコーパスに適用します。
実験により, 微調整モデルにより, UT生成効率が高いことを示す。
論文 参考訳（メタデータ） (2026-02-03T06:52:54Z) - EquiBench: Benchmarking Large Language Models' Reasoning about Program Semantics via Equivalence Checking [58.15568681219339]
大規模言語モデル(LLM)を評価するための新しいベンチマークであるEquiBenchを紹介する。
このタスクは、プログラムのセマンティクスについて推論するモデルの能力を直接テストする。
19の最先端LCMを評価し、最も難しいカテゴリでは、最高の精度は63.8%と76.2%であり、50%のランダムベースラインよりわずかに高い。
論文 参考訳（メタデータ） (2025-02-18T02:54:25Z) - CLOVER: A Test Case Generation Benchmark with Coverage, Long-Context, and Verification [71.34070740261072]
本稿では,テストケースの生成と完成におけるモデルの能力を評価するためのベンチマークCLOVERを提案する。
ベンチマークはタスク間でのコード実行のためにコンテナ化されています。
論文 参考訳（メタデータ） (2025-02-12T21:42:56Z) - Proving the Coding Interview: A Benchmark for Formally Verified Code Generation [3.5319285228327417]
FVAPPS (Formally Verified Automated Programming Progress Standards, FVAPPS) は,プログラムの記述と正確性を証明するための4715サンプルのベンチマークである。
我々は,機械学習とプログラム合成コミュニティに対して,汎用プログラミング問題とその関連した正当性仕様の解決に挑戦する。
論文 参考訳（メタデータ） (2025-02-08T22:54:58Z) - ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis [50.020850767257095]
本稿では,LLMに様々な粒度で自動化手法を付加するProofAugを提案する。
本手法は,オープンソースのDeep-math-7bベースモデルとIsabelle証明アシスタントを用いて,MiniF2Fベンチマークで検証した。
また、ProofAugのLean 4バージョンを実装し、Kimina-Prover-seek-Distill-1.5Bのパス@1のパフォーマンスを44.3%から50.4%に改善します。
論文 参考訳（メタデータ） (2025-01-30T12:37:06Z) - VerMCTS: Synthesizing Multi-Step Programs using a Verifier, a Large Language Model, and Tree Search [5.389248707675898]
大型言語モデル(LLM)は有用なコードを生成することができるが、しばしばそれらが生成するコードは信頼できない。
本稿では,Dafny と Coq で検証プログラムを生成することで,この問題を解決するための VerMCTS を提案する。
論文 参考訳（メタデータ） (2024-02-13T00:55:14Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。