論文の概要: Loop-Based Slicing and Input-Driven Concretization: An Empirical Study of Termination and Non-Termination Analysis
- arxiv url: http://arxiv.org/abs/2607.08988v1
- Date: Thu, 09 Jul 2026 23:29:19 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-07-13 14:47:12.75671
- Title: Loop-Based Slicing and Input-Driven Concretization: An Empirical Study of Termination and Non-Termination Analysis
- Title（参考訳）: ループスライシングと入力駆動型増進:終端解析と非終端解析の実証的研究
- Abstract要約: 本稿では,(非)終端解析のための軽量でツールに依存しないソースレベル前処理の実証的研究について述べる。
ループベースのスライシングを適用したCフロントエンドであるFocusTNTを実装した。
実世界の非終端バグとその修正から派生した117のC/C++プログラム上で,スライシング,コンクリタイズ,および6つのアナライザの組み合わせを評価した。
- 参考スコア（独自算出の注目度）: 1.84316002191515
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Termination and non-termination are fundamental correctness properties, but verifying them in real-world C programs remains difficult because loop interactions and nondeterministic inputs challenge existing analyzers. This paper presents an empirical study of lightweight, tool-independent source-level preprocessing for (non-)termination analysis. We implement FocusTNT, a C front end that applies loop-based slicing to isolate loop-level obligations and input-driven concretization to specialize nondeterministic inputs into selected input-scenario variants. We evaluate slicing, concretization, and their combination across six analyzers on 117 C/C++ programs derived from real-world non-termination bugs and their fixes. The study examines effects on analyzer correctness, complementarity with original-program analysis, loop-level diagnostics, feature sensitivity, runtime behavior, semantic scope, and integration potential. Results show that preprocessing is not uniformly beneficial: its impact depends on the analyzer, task, and program features. Slicing provides conservative structural isolation and localization, whereas concretization can improve detectability for selected scenarios but narrows semantic scope and may increase analysis effort. Their combination is not consistently additive. Overall, the results support adaptive use of preprocessing as a complement to original-program analysis and provide practical guidance to application developers interpreting verification outcomes and tool developers improving analyzer robustness.
- Abstract（参考訳）: 終端と非終端は基本的な正当性の性質であるが、ループ相互作用や非決定論的入力が既存のアナライザに挑戦するため、実世界のCプログラムでの検証は難しいままである。
本稿では,(非)終端解析のための軽量でツールに依存しないソースレベル前処理に関する実証的研究について述べる。
ループベーススライシングを用いてループレベルの義務を分離し,非決定論的入力を選択された入力-scenario バリアントに特殊化する。
実世界の非終端バグとその修正から派生した117のC/C++プログラム上で,スライシング,コンクリタイズ,および6つのアナライザの組み合わせを評価した。
本研究は,アナライザの正しさ,オリジナルプログラム解析との相補性,ループレベルの診断,特徴感度,実行時の振る舞い,意味的スコープ,統合ポテンシャルに与える影響について検討した。
結果は、前処理が一様でないことを示している。その影響はアナライザ、タスク、プログラム機能に依存する。
スライシングは、保守的な構造的分離とローカライゼーションを提供するが、コンクリタイゼーションは、選択されたシナリオに対する検出性を改善するが、セマンティックスコープを狭め、分析の労力を増加させる可能性がある。
それらの組み合わせは一貫して加法的ではない。
全体として、前処理を原プログラム解析の補完として適応的に使用することをサポートし、検証結果を解釈するアプリケーション開発者に実践的なガイダンスを提供し、ツール開発者はアナライザの堅牢性を改善する。
関連論文リスト
- CauSec: Unboxing the Causal Drivers of Static Vulnerability Analysis Performance [51.50254897627053]
静的アプリケーションセキュリティテスト(SAST)ツールは、業界と学術の両方で広く利用されている。
これらのツールは、高いパフォーマンスを達成するために検出を犠牲にする設計上の選択をしばしば行います。
本稿では,これらのツールによる仮定は概して因果性である,というキーとなる考察を頼りに,この問題に対処することを目的とする。
論文 参考訳（メタデータ） (2026-08-19T12:56:00Z) - From Prediction to Collaboration: Interactive Symbolic Music Analysis [8.180530393436326]
記号的ローマ数字RN解析のための統一的なフレームワークを提案する。
強い予測性能と制約付き完了とリビジョンの直接的なサポートを組み合わせる。
完全なスコア分析、既存のラベルのターゲットリビジョン、部分的なコンテキストから欠落したアノテーションの推測をサポートする。
論文 参考訳（メタデータ） (2026-07-15T08:28:43Z) - Finite-Sample Analysis of Nonlinear Independent Component Analysis:Sample Complexity and Identifiability Bounds [1.624454100511275]
独立成分分析(Independent Component Analysis, ICA)は、混合信号を独立したソースに分離することで、データの構造を解明するための基本的な教師なし学習手法である。
学習アルゴリズムの有限サンプル統計特性は未だよく理解されていない。
本稿では,ニューラルネットワークエンコーダを用いた非線形ICAの包括的有限サンプル解析について述べる。
論文 参考訳（メタデータ） (2026-04-10T01:15:27Z) - Dynamic analysis enhances issue resolution [53.50448142467294]
DAIRA(Dynamic Analysis-enhanced Issue Resolution Agent)は、エージェントの推論サイクルに動的解析を組み込む自動修復フレームワークである。
テストトレース駆動の方法論によって駆動されるDAIRAは、軽量モニタを使用して重要なランタイムデータを抽出する。
Gemini 3 Flash Previewを使用すると、DAIRAは新たな最先端(SOTA)パフォーマンスを確立し、SWE-bench Verifiedデータセットで79.4%の解像度を達成する。
論文 参考訳（メタデータ） (2026-03-23T14:48:54Z) - Act, Think or Abstain: Complexity-Aware Adaptive Inference for Vision-Language-Action Models [7.802379200026965]
認識状態の複雑さに基づいてVLA実行を動的にルーティングする適応型フレームワークを提案する。
我々のアプローチは、VLAの視覚言語バックボーンを、パラメトリックおよび非パラメトリック推定器のアンサンブルに潜伏埋め込みを投影することにより、アクティブな検出ツールに変換する。
論文 参考訳（メタデータ） (2026-03-05T13:14:41Z) - Not All Preferences Are Created Equal: Stability-Aware and Gradient-Efficient Alignment for Reasoning Models [52.48582333951919]
ポリシー更新の信号対雑音比を最大化することにより、アライメントの信頼性を高めるために設計された動的フレームワークを提案する。
SAGE(Stability-Aware Gradient Efficiency)は、モデル能力に基づいて候補プールをリフレッシュする粗いきめ細かいカリキュラムメカニズムを統合する。
複数の数学的推論ベンチマークの実験により、SAGEは収束を著しく加速し、静的ベースラインを上回っていることが示された。
論文 参考訳（メタデータ） (2026-02-01T12:56:10Z) - Learning to Align Multi-Faceted Evaluation: A Unified and Robust Framework [61.38174427966444]
大規模言語モデル(LLM)は、様々なシナリオにおける自動評価のために、より広く使われている。
従来の研究では、強力なプロプライエタリモデルの評価と判断を再現するために、オープンソースのLLMを微調整しようと試みてきた。
本稿では,評価基準を適応的に定式化し,テキストベースとコード駆動分析の両方を合成する新しい評価フレームワークARJudgeを提案する。
論文 参考訳（メタデータ） (2025-02-26T06:31:45Z) - Checkification: A Practical Approach for Testing Static Analysis Truths [0.0]
本稿では,抽象解釈に基づく静的アナライザの試験法を提案する。
このアプローチの主な利点は、Ciaoアサーションベースのバリデーションフレームワーク内で直接フレーミングすることによる、シンプルさにあります。
我々は、CiaoPP静的解析器にアプローチを適用し、合理的なオーバーヘッドを伴う多くのバグを特定した。
論文 参考訳（メタデータ） (2025-01-21T12:38:04Z) - Smoothness Analysis for Probabilistic Programs with Application to
Optimised Variational Inference [13.836565669337057]
与えられた確率プログラムの微分可能あるいはより一般に滑らかな部分を発見するための静的解析法を提案する。
解析が経路勾配推定器の改善にどのように役立つかを示す。
論文 参考訳（メタデータ） (2022-08-22T18:18:32Z) - Estimating Structural Target Functions using Machine Learning and
Influence Functions [103.47897241856603]
統計モデルから特定可能な関数として生じる対象関数の統計的機械学習のための新しい枠組みを提案する。
このフレームワークは問題とモデルに依存しないものであり、応用統計学における幅広い対象パラメータを推定するのに使用できる。
我々は、部分的に観測されていない情報を持つランダム/二重ロバストな問題において、いわゆる粗大化に特に焦点をあてた。
論文 参考訳（メタデータ） (2020-08-14T16:48:29Z) - Causal Feature Selection for Algorithmic Fairness [61.767399505764736]
データ管理の統合コンポーネントにおける公平性について検討する。
本稿では,データセットの公平性を保証する特徴のサブコレクションを同定する手法を提案する。
論文 参考訳（メタデータ） (2020-06-10T20:20:10Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。