Fugu-MT 論文翻訳(概要): Computation Tree Logic Guided Program Repair

論文の概要: Computation Tree Logic Guided Program Repair

arxiv url: http://arxiv.org/abs/2502.15344v1
Date: Fri, 21 Feb 2025 09:59:38 GMT
ステータス: 翻訳完了
システム内更新日: 2025-02-24 16:10:30.606469
Title: Computation Tree Logic Guided Program Repair
Title（参考訳）: 計算木論理によるプログラム修復
Authors: Yu Liu, Yahui Song, Martin Mirchev, Abhik Roychoudhury,
Abstract要約: 本稿では,CTL特性によって誘導される無限状態プログラムの自動修復機構を提案する。我々のフレームワークは,プログラムとCTLプロパティをDatalogのファクトとルールにエンコードし,解析ルールをパスするために事実を変更することで修復を行う。提案手法は,小規模ベンチマークでは56.6%,実世界のベンチマークでは88.5%であり,ベースライン性能は27.7%,76.9%であった。
参考スコア（独自算出の注目度）: 10.880298593486671
License:
Abstract: Temporal logics like Computation Tree Logic (CTL) have been widely used as expressive formalisms to capture rich behavioral specifications. CTL can express properties such as reachability, termination, invariants and responsiveness, which are difficult to test. This paper suggests a mechanism for the automated repair of infinite-state programs guided by CTL properties. Our produced patches avoid the overfitting issue that occurs in test-suite-guided repair, where the repaired code may not pass tests outside the given test suite. To realize this vision, we propose a repair framework based on Datalog, a widely used domain-specific language for program analysis, which readily supports nested fixed-point semantics of CTL via stratified negation. Specifically, our framework encodes the program and CTL properties into Datalog facts and rules and performs the repair by modifying the facts to pass the analysis rules. Previous research proposed a generic repair mechanism for Datalog-based analysis in the form of Symbolic Execution of Datalog (SEDL). However, SEDL only supports positive Datalog, which is insufficient for expressing CTL properties. Thus, we extended SEDL to make it applicable to stratified Datalog. Moreover, liveness property violations involve infinite computations, which we handle via a novel loop summarization. Our approach achieves analysis accuracy of 56.6% on a small-scale benchmark and 88.5% on a real-world benchmark, outperforming the best baseline performances of 27.7% and 76.9%. Our approach repairs all detected bugs, which is not achieved by existing tools.
Abstract（参考訳）: 計算木論理(CTL)のような時間論理は、リッチな行動仕様を捉えるための表現形式として広く使われている。 CTLは、テストが難しい到達性、終了性、不変性、応答性などの特性を表現できる。本稿では,CTL特性によって誘導される無限状態プログラムの自動修復機構を提案する。生成されたパッチは、修理済みのコードが所定のテストスイートの外でテストに合格しない場合に発生する過度に適合する問題を回避します。このビジョンを実現するために,プログラム解析に広く使われているドメイン固有言語であるDatalogに基づく修復フレームワークを提案する。具体的には、プログラムとCTLプロパティをDatalogのファクトとルールにエンコードし、解析ルールをパスするために事実を変更することで修復を行う。従来の研究では、データログのシンボル実行(SEDL)という形で、データログ解析のための汎用的な修復機構が提案されていた。しかし、SEDLはCTLプロパティを表現するのに不十分な正のDatalogしかサポートしていない。そこで我々はSEDLを拡張して階層データログに適用した。さらに、生きた性質の違反は無限の計算を伴い、新しいループの要約によって処理する。提案手法は,小規模ベンチマークでは56.6%,実世界のベンチマークでは88.5%であり,ベースライン性能は27.7%,76.9%であった。当社のアプローチでは,検出されたすべてのバグを修復していますが,既存のツールでは実現できません。

関連論文リスト

Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis [50.020850767257095]
本稿では,より優れたサンプル効率を有する定理証明手法であるProofAugを提案する。本手法は,オープンソースのDeepseek-math-7bベースモデルとIsabelle証明アシスタントを用いて,miniF2F-testベンチマークで検証した。
論文参考訳（メタデータ） (2025-01-30T12:37:06Z)
StructTest: Benchmarking LLMs' Reasoning through Compositional Structured Outputs [78.84060166851805]
StructTestは、構造化されたアウトプットを生成する能力に基づいて、大きな言語モデルを評価する新しいベンチマークである。 StructTestが一般的な推論能力のよいプロキシであることを示す。
論文参考訳（メタデータ） (2024-12-23T22:08:40Z)
Enhancing Automated Loop Invariant Generation for Complex Programs with Large Language Models [2.243213786359577]
ACInvは、自動複雑プログラムループ不変生成ツールである。静的解析とLLM(Large Language Models)を組み合わせることで、適切なループ不変量を生成する。我々はACInvの実験を行い、ACInvはデータ構造を持つデータセットにおいて、以前のツールよりも優れていたことを示した。
論文参考訳（メタデータ） (2024-12-13T10:36:18Z)
VerilogCoder: Autonomous Verilog Coding Agents with Graph-based Planning and Abstract Syntax Tree (AST)-based Waveform Tracing Tool [4.027984601764008]
We propose VerilogCoder, a system of multiple Artificial Intelligence (AI) agent for Verilog code generation。提案手法は、構文的に94.2%、機能的に正当なVerilogコードを生成する。
論文参考訳（メタデータ） (2024-08-15T20:06:06Z)
Fix the Tests: Augmenting LLMs to Repair Test Cases with Static Collector and Neural Reranker [9.428021853841296]
本稿では, TROCtxsの精密かつ高精度な構築により, 旧来の検査ケースを自動的に修復する新しい手法であるSynTERを提案する。構築されたTROCtxの増強により、幻覚は57.1%減少する。
論文参考訳（メタデータ） (2024-07-04T04:24:43Z)
Data is all you need: Finetuning LLMs for Chip Design via an Automated design-data augmentation framework [50.02710905062184]
本稿では,Verilog と EDA スクリプトに適合する高ボリュームかつ高品質な自然言語を生成する自動設計データ拡張フレームワークを提案する。 Verilog生成の精度は現在の最先端のオープンソースVerilog生成モデルを超え、同じベンチマークで58.8%から70.6%に増加した。
論文参考訳（メタデータ） (2024-03-17T13:01:03Z)
Supporting Error Chains in Static Analysis for Precise Evaluation Results and Enhanced Usability [2.8557828838739527]
静的解析は、固定位置よりも脆弱性が現れる場所を報告する傾向にある。これは仮定された偽陽性や不正確な結果を引き起こす可能性がある。我々は、既存の静的解析アルゴリズムを適応させ、マニフェストと固定位置を区別できるように設計した。
論文参考訳（メタデータ） (2024-03-12T16:46:29Z)
RAP-Gen: Retrieval-Augmented Patch Generation with CodeT5 for Automatic Program Repair [75.40584530380589]
新たな検索型パッチ生成フレームワーク(RAP-Gen)を提案する。 RAP-Gen 以前のバグ修正ペアのリストから取得した関連する修正パターンを明示的に活用する。 RAP-GenをJavaScriptのTFixベンチマークとJavaのCode RefinementとDefects4Jベンチマークの2つのプログラミング言語で評価する。
論文参考訳（メタデータ） (2023-09-12T08:52:56Z)
Timing Analysis of Embedded Software Updates [1.7027593388928293]
組込みソフトウェアの実行時間に対する更新の影響を検証するための差分タイミング解析手法であるRETAを提案する。我々は、産業タイミング分析ツールであるaiTへのRETAの統合に適応し、DELTAと呼ばれるツールで完全な実装を開発する。一方,RETA を DELTA から削除することで,リアルタイム解析ツールとして有効に活用し,解析時間を27% 向上させる。
論文参考訳（メタデータ） (2023-04-27T14:19:15Z)
Linear Temporal Logic Modulo Theories over Finite Traces (Extended Version) [72.38188258853155]
有限トレース(LTLf)上の線形時間論理について検討する。命題の文字は任意の理論で解釈された一階述語式に置き換えられる。 Satisfiability Modulo Theories (LTLfMT) と呼ばれる結果の論理は半決定可能である。
論文参考訳（メタデータ） (2022-04-28T17:57:33Z)
Self-Supervised Log Parsing [59.04636530383049]
大規模ソフトウェアシステムは、大量の半構造化ログレコードを生成する。既存のアプローチは、ログ特化や手動ルール抽出に依存している。本稿では,自己教師付き学習モデルを用いて解析タスクをマスク言語モデリングとして定式化するNuLogを提案する。
論文参考訳（メタデータ） (2020-03-17T19:25:25Z)

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

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