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 23:44:09.978934
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: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
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%であった。当社のアプローチでは,検出されたすべてのバグを修復していますが,既存のツールでは実現できません。

関連論文リスト

The Hitchhiker's Guide to Program Analysis, Part II: Deep Thoughts by LLMs [17.497629884237647]
BugLensは、静的解析の精度を大幅に改善する、ポストリファインメントフレームワークである。 0.10 (raw) と 0.50 (半自動精製) から 0.72 に精度を上げ、偽陽性を著しく減少させる。この結果から,構造化LCMベースのワークフローは静的解析ツールの有効性を有意に向上させることができることが示唆された。
論文参考訳（メタデータ） (2025-04-16T02:17:06Z)
GateLens: A Reasoning-Enhanced LLM Agent for Automotive Software Release Analytics [9.549568621873386]
GateLensはAlgebraベースのツールで、自動車分野のデータセットを分析する。高いF1スコアを達成し、より堅牢な複雑で曖昧なクエリを処理する。高い精度と信頼性を維持しながら、分析時間を80%以上削減する。
論文参考訳（メタデータ） (2025-03-27T17:48:32Z)
CASTLE: Benchmarking Dataset for Static Code Analyzers and LLMs towards CWE Detection [2.5228276786940182]
本稿では,異なる手法の脆弱性検出能力を評価するためのベンチマークフレームワークであるCASTLEを紹介する。我々は,25個のCWEをカバーする250個のマイクロベンチマークプログラムを手作りしたデータセットを用いて,静的解析ツール13,LLM10,形式検証ツール2を評価した。
論文参考訳（メタデータ） (2025-03-12T14:30:05Z)
Learning to Solve and Verify: A Self-Play Framework for Code and Test Generation [69.62857948698436]
大規模言語モデル(LLM)の最近の進歩は、コーディングベンチマークのパフォーマンスを改善している。しかし、手軽に利用できる高品質なデータの枯渇により、改善は停滞している。本稿では,単一モデルのコードとテスト生成能力を共同で改善するセルフプレイ・ソルバ検証フレームワークであるSol-Verを提案する。
論文参考訳（メタデータ） (2025-02-20T18:32:19Z)
Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis [50.020850767257095]
本稿では,より優れたサンプル効率を有する定理証明手法であるProofAugを提案する。本手法は,オープンソースのDeepseek-math-7bベースモデルとIsabelle証明アシスタントを用いて,miniF2F-testベンチマークで検証した。
論文参考訳（メタデータ） (2025-01-30T12:37:06Z)
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)
LLMDFA: Analyzing Dataflow in Code with Large Language Models [8.92611389987991]
本稿では,コンパイル不要でカスタマイズ可能なデータフロー解析フレームワークLLMDFAを提案する。問題をいくつかのサブタスクに分解し、一連の新しい戦略を導入する。 LLMDFAは平均87.10%の精度と80.77%のリコールを達成し、F1スコアを最大0.35に向上させた。
論文参考訳（メタデータ） (2024-02-16T15:21:35Z)
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)

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

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