論文の概要: Array-Carrying Symbolic Execution for Function Contract Generation

• arxiv url: http://arxiv.org/abs/2602.23216v1
• Date: Thu, 26 Feb 2026 17:00:10 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-02-27 18:41:22.796884
• Title: Array-Carrying Symbolic Execution for Function Contract Generation
• Title（参考訳）: 関数契約生成のためのアレーキャリングシンボリック実行
• Authors: Weijie Lu, Jingyu Ke, Hongfei Fu, Zhouyue Sun, Yi Zhou, Guoqiang Li, Haokun Li,
• Abstract要約: 本稿では,不変変数を格納し,配列の連続セグメントに情報を割り当てる新しいシンボリック実行フレームワークを提案する。 我々は,LLVMのプロトタイプとしてフレームワークを実装し,そのプロトタイプをACSLアサーションフォーマットとFrama-Cソフトウェア検証プラットフォームに統合する。
• 参考スコア（独自算出の注目度）: 4.472707897843483
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Function contract generation is a classical problem in program analysis that targets the automated analysis of functions in a program with multiple procedures. The problem is fundamental in inter-procedural analysis where properties of functions are first obtained via the generation of function contracts and then the generated contracts are used as building blocks to analyze the whole program. Typical objectives in function contract generation include pre-/post-conditions and assigns information (that specifies the modification information over program variables and memory segments during function execution). In programs with array manipulations, a crucial point in function contract generation is the treatment of array segments that imposes challenges in inferring invariants and assigns information over such segments. To address this challenge, we propose a novel symbolic execution framework that carries invariants and assigns information over contiguous segments of arrays. We implement our framework as a prototype within LLVM, and further integrate our prototype with the ACSL assertion format and the Frama-C software verification platform. Experimental evaluation over a variety of benchmarks from the literature and functions from realistic libraries shows that our framework is capable of handling array manipulating functions that indeed involve the carry of array information and are beyond existing approaches.
• Abstract（参考訳）: 関数コントラクト生成(英: function contract generation)は、プログラム解析における古典的な問題であり、複数のプロシージャを持つプログラムにおける関数の自動解析を目標とする。 この問題は、関数のプロパティが関数コントラクトの生成によって最初に取得され、次に生成されたコントラクトがプログラム全体を解析するためのビルディングブロックとして使用される、プロセス間解析において基本的なものである。 関数コントラクト生成の典型的な目的は、プリ/ポスト条件を含み、情報(関数実行中にプログラム変数やメモリセグメントに対して変更情報を指定する)を割り当てる。 配列操作を伴うプログラムにおいて、関数コントラクト生成の重要なポイントは、不変性を推論し、そのようなセグメントに情報を割り当てる際の課題を課す配列セグメントの処理である。 この課題に対処するために,不変量を持ち,配列の連続セグメントに情報を割り当てる新しいシンボリック実行フレームワークを提案する。 我々は,LLVMのプロトタイプとしてフレームワークを実装し,そのプロトタイプをACSLアサーションフォーマットとFrama-Cソフトウェア検証プラットフォームに統合する。 現実的なライブラリの文献や関数の様々なベンチマークに対する実験的な評価は、我々のフレームワークが配列情報の搬送を実際に含む配列操作関数を処理でき、既存のアプローチを超えていることを示している。

関連論文リスト

• Automated Synthesis of Formally Verified Multi-Abstraction Function Summaries [19.23701821549906]
  本稿では,記号実行,大規模言語モデル(LLM),および相対的最強ポストコンディション(RSP)を生成するための形式検証を組み合わせた新しいフレームワークを提案する。 我々のアプローチは、VST-Aのシンボル的実行を利用して、プログラムの実行パスと状態遷移を正確に追跡する。 生成したRSPから,ドメイン固有言語内で表現される最強の非冗長な条件を自動で合成する。
  論文  参考訳（メタデータ） (2025-06-11T09:33:02Z)
• Beyond the Edge of Function: Unraveling the Patterns of Type Recovery in Binary Code [55.493408628371235]
  本稿では,バイナリコードの変数型を復元するフレームワークByteTRを提案する。 ByteTRは、関数間の変数伝搬の普遍性を考慮して、変数伝搬をトレースするためのプロシーダ間解析を行い、ゲートグラフニューラルネットワークを用いて、変数型回復のための長距離データフロー依存性をキャプチャする。
  論文  参考訳（メタデータ） (2025-03-10T12:27:05Z)
• C Analyzer : A Static Program Analysis Tool for C Programs [0.0]
  C Analyzerは、Cプログラムの静的解析のために開発されたツールである。 本研究は,Cプログラムの静的解析に抽象解釈技術を活用することを目的とする。
  論文  参考訳（メタデータ） (2024-01-28T11:43:16Z)
• UniRef++: Segment Every Reference Object in Spatial and Temporal Spaces [92.52589788633856]
  単一のアーキテクチャで4つの参照ベースのオブジェクトセグメンテーションタスクを統合するために、UniRef++を提案する。 統一された設計により、UniRef++は幅広いベンチマークで共同でトレーニングすることができ、実行時に柔軟に複数のタスクを完了させることができる。 提案する UniRef++ は RIS と RVOS の最先端性能を実現し,パラメータ共有ネットワークを用いて FSS と VOS の競合性能を実現する。
  論文  参考訳（メタデータ） (2023-12-25T12:54:11Z)
• Multi-level Reasoning for Robotic Assembly: From Sequence Inference to Contact Selection [74.40109927350856]
  本稿では,PAST(Part Assembly Sequence Transformer)を用いて,対象とするブループリントからアセンブリシーケンスを推論する。 次に、モーションプランナーと最適化を使用して、部品の動きと接触を生成する。 実験結果から,本手法は従来手法よりも一般化されていることがわかった。
  論文  参考訳（メタデータ） (2023-12-17T00:47:13Z)
• FIND: A Function Description Benchmark for Evaluating Interpretability Methods [86.80718559904854]
  本稿では,自動解釈可能性評価のためのベンチマークスイートであるFIND(Function Interpretation and Description)を紹介する。 FINDには、トレーニングされたニューラルネットワークのコンポーネントに似た機能と、私たちが生成しようとしている種類の記述が含まれています。 本研究では、事前訓練された言語モデルを用いて、自然言語とコードにおける関数の振る舞いの記述を生成する手法を評価する。
  論文  参考訳（メタデータ） (2023-09-07T17:47:26Z)
• Better Context Makes Better Code Language Models: A Case Study on Function Call Argument Completion [15.068025336990287]
  既存のコード補完モデルでは、完了タスクに良い結果が得られないことを示します。 与えられた関数呼び出しに関する情報をプログラムアナライザに問い合わせ、推論およびトレーニング中に異なるコード補完モデルに対してアナライザ結果を提供する方法を検討する。 実験の結果,関数の実装と関数の使用量へのアクセスは,引数補完性能を大幅に向上させることがわかった。
  論文  参考訳（メタデータ） (2023-06-01T06:25:58Z)
• A Mechanistic Interpretation of Arithmetic Reasoning in Language Models using Causal Mediation Analysis [128.0532113800092]
  算数問題に対するトランスフォーマーに基づくLMの機械的解釈を提案する。 これにより、算術に関連する情報がLMによってどのように処理されるかについての洞察が得られる。
  論文  参考訳（メタデータ） (2023-05-24T11:43:47Z)
• Representing Partial Programs with Blended Abstract Semantics [62.20775388513027]
  プログラム合成エンジンにおける部分的なプログラム表現手法について紹介する。 モジュラーニューラルネットワークとして実装された近似実行モデルを学ぶ。 これらのハイブリッドニューロシンボリック表現は、実行誘導型シンセサイザーがより強力な言語構成を使うことができることを示す。
  論文  参考訳（メタデータ） (2020-12-23T20:40:18Z)

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

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