論文の概要: Automated Synthesis of Formally Verified Multi-Abstraction Function Summaries

• arxiv url: http://arxiv.org/abs/2506.09550v1
• Date: Wed, 11 Jun 2025 09:33:02 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-06-13 06:35:02.810456
• Title: Automated Synthesis of Formally Verified Multi-Abstraction Function Summaries
• Title（参考訳）: 形式的検証多重抽象関数の自動合成
• Authors: Fanpeng Yang, Xu Ma, Shuling Wang, Xiong Xu, Qinxiang Cao, Naijun Zhan, Xiaofeng Li, Bin Gu,
• Abstract要約: 本稿では,記号実行,大規模言語モデル(LLM),および相対的最強ポストコンディション(RSP)を生成するための形式検証を組み合わせた新しいフレームワークを提案する。 我々のアプローチは、VST-Aのシンボル的実行を利用して、プログラムの実行パスと状態遷移を正確に追跡する。 生成したRSPから,ドメイン固有言語内で表現される最強の非冗長な条件を自動で合成する。
• 参考スコア（独自算出の注目度）: 19.23701821549906
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Function summaries, which characterize the behavior of code segments (typically functions) through preconditions and postconditions, are essential for understanding, reusing, and verifying software, particularly in safety-critical domains like aerospace embedded systems. However, these mission-critical legacy code serving as a valuable reused asset often lacks formal specifications. It is challenging to automatically generate function summaries for C programs, due to the existence of complex features such as loops, nested function calls, pointer aliasing, and so on. Moreover, function summaries should support multiple abstraction levels to meet diverse requirements, e.g. precise summaries capturing full functionality for formal verification and intuitive summaries for human understanding. To address these challenges, we first propose a novel framework that combines symbolic execution, large language models (LLMs), and formal verification to generate Relatively Strongest Postconditions (RSPs) and build function summaries that fully capture program behavior. Our approach leverages VST-A's symbolic execution to precisely track program execution paths and state transitions, employs LLMs to infer loop invariants based on predefined templates, and uses Frama-C to guarantee soundness of generated summaries in an iterative refinement loop. Furthermore, from generated RSPs, we automatically synthesize strongest non-redundant postconditions expressed within given domain specific language. We compare our approach with existing work through extensive experiments.
• Abstract（参考訳）: 関数要約(英: function summaries)は、プリコンディションやポストコンディションを通じてコードセグメント(典型的には関数)の振る舞いを特徴付けるものであり、特に航空宇宙組み込みシステムのような安全クリティカルな領域において、ソフトウェアを理解し、再利用し、検証するために不可欠である。 しかし、これらのミッションクリティカルなレガシーコードは、価値ある再利用資産として機能し、しばしば正式な仕様を欠いている。 ループ、ネストされた関数呼び出し、ポインタエイリアスなどの複雑な機能があるため、Cプログラムの関数要約を自動的に生成することは難しい。 さらに、機能要約は、様々な要件を満たすために、複数の抽象化レベルをサポートする必要がある。 これらの課題に対処するために,我々はまず,記号実行,大規模言語モデル(LLM),およびプログラム動作を完全にキャプチャする相対的最強ポストコンディション(RSP)を生成するための形式検証を組み合わせた新しいフレームワークを提案する。 提案手法では,プログラム実行パスと状態遷移を正確に追跡するためにVST-Aのシンボリック実行を活用し,予め定義されたテンプレートに基づいてループ不変量を推定するためにLLMを採用し,Frama-Cを用いて繰り返し精製ループにおいて生成された要約の健全性を保証する。 さらに、生成されたRSPから、与えられたドメイン固有言語内で表現される最強の非冗長な条件を自動で合成する。 当社のアプローチを,広範な実験を通じて既存の作業と比較する。

関連論文リスト

• CodeARC: Benchmarking Reasoning Capabilities of LLM Agents for Inductive Program Synthesis [6.8081984950459]
  大規模言語モデルエージェントは、自然言語でガイドされるプログラミングタスクにおいて有望であることを示している。 既存の評価プロトコルは、静的なサンプルセットとホールドアウトテストに依存している。 エージェントが隠れたターゲット関数と相互作用する新しい評価フレームワークであるCodeARCを提案する。
  論文  参考訳（メタデータ） (2025-03-29T16:50:39Z)
• Learning Task Representations from In-Context Learning [73.72066284711462]
  大規模言語モデル(LLM)は、文脈内学習において顕著な習熟性を示している。 ICLプロンプトにおけるタスク情報をアテンションヘッドの関数として符号化するための自動定式化を導入する。 提案手法の有効性は,最後の隠れ状態の分布と最適に実行されたテキスト内学習モデルとの整合性に起因していることを示す。
  論文  参考訳（メタデータ） (2025-02-08T00:16:44Z)
• EpiCoder: Encompassing Diversity and Complexity in Code Generation [49.170195362149386]
  既存のコード生成方法はシードデータとしてコードスニペットを使用する。 階層的なコード機能を中心に展開する,新しい機能ツリーベースの合成フレームワークを提案する。 我々のフレームワークは、生成されたコードの複雑さを正確に制御し、関数レベルの操作からマルチファイルのシナリオまで幅広い機能を実現する。
  論文  参考訳（メタデータ） (2025-01-08T18:58:15Z)
• Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification [15.686651364655958]
  AutoSpecは、自動プログラム検証のための仕様を合成するための自動化アプローチである。 仕様の汎用性における既存の作業の欠点を克服し、完全な証明のために十分かつ適切な仕様を合成する。 実世界のX509パーサプロジェクトでプログラムを検証するためにうまく適用することができる。
  論文  参考訳（メタデータ） (2024-03-31T18:15:49Z)
• Synthesizing Efficiently Monitorable Formulas in Metric Temporal Logic [4.60607942851373]
  システム実行から形式仕様を自動合成する問題を考察する。 時間論理式を合成するための古典的なアプローチの多くは、公式のサイズを最小化することを目的としている。 我々は,この概念を定式化し,有界な外見を持つ簡潔な公式を合成する学習アルゴリズムを考案する。
  論文  参考訳（メタデータ） (2023-10-26T14:13:15Z)
• Self-regulating Prompts: Foundational Model Adaptation without Forgetting [112.66832145320434]
  本稿では,PromptSRCと呼ばれる自己正規化フレームワークを提案する。 PromptSRCはタスク固有の汎用表現とタスクに依存しない汎用表現の両方に最適化するプロンプトを導く。
  論文  参考訳（メタデータ） (2023-07-13T17:59:35Z)
• Large Language Models as General Pattern Machines [64.75501424160748]
  我々は,事前訓練された大規模言語モデル (LLM) が,複雑なトークンシーケンスを自動回帰的に完了することを示す。 驚いたことに、語彙からランダムにサンプリングされたトークンを用いてシーケンスが表現された場合でも、パターン完了の習熟度を部分的に保持することができる。 本研究では,ロボット工学における問題に対して,これらのゼロショット機能がどのように適用されるかを検討する。
  論文  参考訳（メタデータ） (2023-07-10T17:32:13Z)
• Denoising-Contrastive Alignment for Continuous Sign Language Recognition [22.800767994061175]
  連続手話認識は,手話ビデオからテキストグルースへの符号認識を目的としている。 現在のクロスモダリティアライメントパラダイムは、ビデオ表現を導くためにテキスト文法の役割を無視することが多い。 本稿では,映像の表現性を高めるために,Denoising-Contrastive Alignmentパラダイムを提案する。
  論文  参考訳（メタデータ） (2023-05-05T15:20:27Z)
• Summarization Programs: Interpretable Abstractive Summarization with Neural Modular Trees [89.60269205320431]
  現在の抽象的要約モデルは明確な解釈可能性の欠如に悩まされるか、あるいは不完全理性を与える。 本稿では,バイナリツリーの(順序付き)リストからなる解釈可能なモジュラーフレームワークであるSummarization Program (SP)を提案する。 要約プログラムは、要約文毎に1つのルートノードを含み、各要約文と文書文を個別のツリーで接続する。
  論文  参考訳（メタデータ） (2022-09-21T16:50:22Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。