論文の概要: Cache-a-lot: Pushing the Limits of Unsatisfiable Core Reuse in SMT-Based Program Analysis

• arxiv url: http://arxiv.org/abs/2504.07642v1
• Date: Thu, 10 Apr 2025 10:43:42 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-04-11 12:22:28.694220
• Title: Cache-a-lot: Pushing the Limits of Unsatisfiable Core Reuse in SMT-Based Program Analysis
• Title（参考訳）: Cache-a-lot:SMTプログラム解析における不満足なコア再利用の限界を押し上げる
• Authors: Rustam Sadykov, Azat Abdullin, Marat Akhin,
• Abstract要約: Satisfiability Modulo Theories (SMT) は、ココリックやシンボリックな実行のようなプログラム分析技術に不可欠な解法である。 キャッシュ・ア・ロット(Cache-a-lot)という新しい手法を提案し,全ての可能な変数置換を体系的に検討することによって,不満足な(不満足な)結果の再利用を拡大する。
• 参考スコア（独自算出の注目度）: 2.867517731896504
• License:
• Abstract: Satisfiability Modulo Theories (SMT) solvers are integral to program analysis techniques like concolic and symbolic execution, where they help assess the satisfiability of logical formulae to explore execution paths of the program under test. However, frequent solver invocations are still the main performance bottleneck of these techniques. One way to mitigate this challenge is through optimizations such as caching and reusing solver results. While current methods typically focus on reusing results from fully equivalent or closely related formulas, they often miss broader opportunities for reuse. In this paper, we propose a novel approach, Cache-a-lot, that extends the reuse of unsatisfiable (unsat) results by systematically considering all possible variable substitutions. This enables more extensive reuse of results, thereby reducing the number of SMT solver invocations and improving the overall efficiency of concolic and symbolic execution. Our evaluation, conducted against the state-of-the-art Utopia solution using two benchmark sets, shows significant improvements, particularly with more complex formulas. Our method achieves up to 74% unsat core reuse, compared to Utopia's 41%, and significant increase in the time savings. These results demonstrate that, despite the additional computational complexity, the broader reuse of unsat results significantly enhances performance, offering valuable advancements for formal verification and program analysis.
• Abstract（参考訳）: SMT(Satifiability Modulo Theories)は、ココリックやシンボリックな実行のようなプログラム解析手法に不可欠な解法であり、論理式の満足度を評価し、テスト中のプログラムの実行経路を探索する。 しかし、これらの技術の主なパフォーマンスボトルネックは、頻繁なソルバ呼び出しである。 この課題を軽減する方法の1つは、キャッシュやソルバ結果の再利用といった最適化を通じてである。 現在の手法は一般的に、完全に等価あるいは密接に関連する公式の結果の再利用に重点を置いているが、しばしば再利用の機会を逃している。 本稿では,全ての変数置換を体系的に検討し,不満足な(不満足な)結果の再利用を拡張する新しいアプローチであるCache-a-lotを提案する。 これにより、より広範な結果の再利用が可能となり、SMTソルバの呼び出し数が減少し、ココリックおよびシンボリック実行の全体的な効率が向上する。 2つのベンチマークセットを用いて,最先端のユートピアソリューションに対する評価を行ったところ,特に複雑な式では,大幅な改善が見られた。 提案手法は, ユトピアの41%に比べて最大74%の未飽和コア再利用を実現し, 省エネ効果が著しく向上した。 これらの結果は,計算複雑性が増大しているにもかかわらず,不満足な結果のより広範な再利用は性能を著しく向上させ,形式的検証やプログラム解析に有用な進歩をもたらすことを示した。

関連論文リスト

• LLaMA-Berry: Pairwise Optimization for O1-like Olympiad-Level Mathematical Reasoning [56.273799410256075]
  このフレームワークはMonte Carlo Tree Search (MCTS)と反復的なSelf-Refineを組み合わせて推論パスを最適化する。 このフレームワークは、一般的なベンチマークと高度なベンチマークでテストされており、探索効率と問題解決能力の点で優れた性能を示している。
  論文  参考訳（メタデータ） (2024-10-03T18:12:29Z)
• OptEx: Expediting First-Order Optimization with Approximately Parallelized Iterations [12.696136981847438]
  ほぼ並列化されたイテレーション (OptEx) で高速化された一階最適化を導入する。 OptExは、並列コンピューティングを活用して、その反復的ボトルネックを軽減することで、FOOの効率を高める最初のフレームワークである。 我々は、カーネル化された勾配推定の信頼性とSGDベースのOpsExの複雑さを理論的に保証する。
  論文  参考訳（メタデータ） (2024-02-18T02:19:02Z)
• Analyzing and Enhancing the Backward-Pass Convergence of Unrolled Optimization [50.38518771642365]
  ディープネットワークにおけるコンポーネントとしての制約付き最適化モデルの統合は、多くの専門的な学習タスクに有望な進歩をもたらした。 この設定における中心的な課題は最適化問題の解によるバックプロパゲーションであり、しばしば閉形式を欠いている。 本稿では, 非線形最適化の後方通過に関する理論的知見を提供し, 特定の反復法による線形システムの解と等価であることを示す。 Folded Optimizationと呼ばれるシステムが提案され、非ローリングなソルバ実装からより効率的なバックプロパゲーションルールを構築する。
  論文  参考訳（メタデータ） (2023-12-28T23:15:18Z)
• Unexpected Improvements to Expected Improvement for Bayesian Optimization [21.901803477674264]
  提案するLogEIは,メンバが標準値と同一あるいはほぼ等しい最適値を持つが,数値的最適化が極めて容易な,新たな獲得関数群である。 実験結果から,LogEIファミリーの獲得関数は,標準関数の最適化性能を大幅に向上し,最近の最先端の獲得関数の性能に匹敵する結果が得られた。
  論文  参考訳（メタデータ） (2023-10-31T17:59:56Z)
• Performance Embeddings: A Similarity-based Approach to Automatic Performance Optimization [71.69092462147292]
  パフォーマンス埋め込みは、アプリケーション間でパフォーマンスチューニングの知識伝達を可能にする。 本研究では, 深層ニューラルネットワーク, 密度およびスパース線形代数合成, および数値風速予測ステンシルのケーススタディにおいて, この伝達チューニング手法を実証する。
  論文  参考訳（メタデータ） (2023-03-14T15:51:35Z)
• Metric Compatible Training for Online Backfilling in Large-Scale Retrieval [67.72644952719791]
  バックフィルは、画像検索システムにおいて、アップグレードされたモデルからすべてのギャラリー埋め込みを再抽出するプロセスである。 本稿では,オンラインのバックフィルアルゴリズムを提案し,バックフィル処理の進行的な性能向上を実現する。 我々は、逆変換モジュールをより効果的で効率的なマージに組み込み、メトリック互換のコントラスト学習アプローチを採用することでさらに強化する。
  論文  参考訳（メタデータ） (2023-01-10T03:10:32Z)
• Loop Unrolled Shallow Equilibrium Regularizer (LUSER) -- A Memory-Efficient Inverse Problem Solver [26.87738024952936]
  逆問題では、潜在的に破損し、しばしば不適切な測定結果から、いくつかの基本的な関心のシグナルを再構築することを目的としている。 浅い平衡正規化器(L)を用いたLUアルゴリズムを提案する。 これらの暗黙のモデルは、より深い畳み込みネットワークと同じくらい表現力があるが、トレーニング中にはるかにメモリ効率が良い。
  論文  参考訳（メタデータ） (2022-10-10T19:50:37Z)
• Efficient Neural Network Analysis with Sum-of-Infeasibilities [64.31536828511021]
  凸最適化における総和係数法に着想を得て,広範な分岐関数を持つネットワーク上での検証クエリを解析するための新しい手法を提案する。 標準ケース分析に基づく完全探索手順の拡張は、各検索状態で実行される凸手順をDeepSoIに置き換えることによって達成できる。
  論文  参考訳（メタデータ） (2022-03-19T15:05:09Z)
• Stochastic Reweighted Gradient Descent [4.355567556995855]
  SRG(stochastic reweighted gradient)と呼ばれる重要サンプリングに基づくアルゴリズムを提案する。 我々は、提案手法の時間とメモリオーバーヘッドに特に注意を払っています。 我々はこの発見を裏付ける実験結果を示す。
  論文  参考訳（メタデータ） (2021-03-23T04:09:43Z)
• Combining Deep Learning and Optimization for Security-Constrained Optimal Power Flow [94.24763814458686]
  セキュリティに制約のある最適電力フロー(SCOPF)は、電力システムの基本である。 SCOPF問題におけるAPRのモデル化は、複雑な大規模混合整数プログラムをもたらす。 本稿では,ディープラーニングとロバスト最適化を組み合わせた新しい手法を提案する。
  論文  参考訳（メタデータ） (2020-07-14T12:38:21Z)

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

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