論文の概要: State Merging with Quantifiers in Symbolic Execution

• arxiv url: http://arxiv.org/abs/2308.12068v2
• Date: Thu, 24 Aug 2023 09:25:35 GMT
• ステータス: 処理完了
• システム内更新日: 2023-10-23 12:54:27.181575
• Title: State Merging with Quantifiers in Symbolic Execution
• Title（参考訳）: シンボリック実行における量子化器による状態マージ
• Authors: David Trabish, Noam Rinetzky, Sharon Shoham, Vaibhav Sharma
• Abstract要約: 状態統合時に導入された解離の数とif-then-else式を減らすことを目的としている。 主なアイデアは、シンボル状態が経路制約で検出された同様の一様構造に従って、動的に合併群に分割することである。
• 参考スコア（独自算出の注目度）: 1.07873286104678
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: We address the problem of constraint encoding explosion which hinders the applicability of state merging in symbolic execution. Specifically, our goal is to reduce the number of disjunctions and if-then-else expressions introduced during state merging. The main idea is to dynamically partition the symbolic states into merging groups according to a similar uniform structure detected in their path constraints, which allows to efficiently encode the merged path constraint and memory using quantifiers. To address the added complexity of solving quantified constraints, we propose a specialized solving procedure that reduces the solving time in many cases. Our evaluation shows that our approach can lead to significant performance gains.
• Abstract（参考訳）: シンボル実行における状態マージの適用性を阻害する制約符号化爆発の問題に対処する。 具体的には、状態統合時に導入された解離の数とif-then-else式を減らすことを目的とする。 主なアイデアは、経路制約で検出される同様の一様構造に従って、シンボリック状態をマージグループに動的に分割することであり、マージされた経路制約とメモリを量子化器を用いて効率的にエンコードできる。 量子化制約を解くことの複雑さに対処するため,多くのケースにおいて解時間を短縮する特殊な解法を提案する。 評価の結果,本手法が性能向上につながる可能性が示唆された。

関連論文リスト

• Hierarchical Context Merging: Better Long Context Understanding for Pre-trained LLMs [61.40047491337793]
  本稿では,大規模言語モデルの制約を克服する新しいトレーニングフリースキームである階層型cOntext MERging(HOMER)を提案する。 HomeRは、長いインプットを管理可能なチャンクに分割する、分別/対数アルゴリズムを使用する。 トークン削減技術がマージ毎に先行し、メモリ使用効率が保証される。
  論文  参考訳（メタデータ） (2024-04-16T06:34:08Z)
• Tractable Bounding of Counterfactual Queries by Knowledge Compilation [51.47174989680976]
  本稿では, パール構造因果モデルにおいて, 因果関係などの部分的特定可能なクエリのバウンダリングの問題について議論する。 最近提案された反復EMスキームは初期化パラメータをサンプリングしてそれらの境界を内部近似する。 シンボルパラメータを実際の値に置き換えた回路構造を,単一のシンボル知識コンパイルによって得られることを示す。
  論文  参考訳（メタデータ） (2023-10-05T07:10:40Z)
• Targeted Control-flow Transformations for Mitigating Path Explosion in Dynamic Symbolic Execution [0.27309692684728615]
  動的シンボリック実行(DSE)は、ターゲットプログラムが多くの条件分岐を持つ場合、経路の爆発的な問題に悩まされる。 本稿では,高コストなシンボル分岐を除去する非意味保存型コンパイラ手法を提案する。
  論文  参考訳（メタデータ） (2023-08-03T06:34:34Z)
• Semantics-Aware Dynamic Localization and Refinement for Referring Image Segmentation [102.25240608024063]
  画像の参照は、言語表現からのイメージセグメントを参照する。 そこで我々は,局所化中心からセグメンテーション言語へ移行するアルゴリズムを開発した。 比較すると,本手法はより汎用的で有効である。
  論文  参考訳（メタデータ） (2023-03-11T08:42:40Z)
• Object Representations as Fixed Points: Training Iterative Refinement Algorithms with Implicit Differentiation [88.14365009076907]
  反復的洗練は表現学習に有用なパラダイムである。 トレーニングの安定性とトラクタビリティを向上させる暗黙の差別化アプローチを開発する。
  論文  参考訳（メタデータ） (2022-07-02T10:00:35Z)
• Algorithm for Constrained Markov Decision Process with Linear Convergence [55.41644538483948]
  エージェントは、そのコストに対する複数の制約により、期待される累積割引報酬を最大化することを目的としている。 エントロピー正規化ポリシーとベイダの二重化という2つの要素を統合した新しい双対アプローチが提案されている。 提案手法は(線形速度で)大域的最適値に収束することが示されている。
  論文  参考訳（メタデータ） (2022-06-03T16:26:38Z)
• Lifting Symmetry Breaking Constraints with Inductive Logic Programming [2.036811219647753]
  我々は、Symmetry Breaking Constraintsを解釈可能な一階制約の集合に引き上げる、Answer Set Programmingのための新しいモデル指向のアプローチを導入する。 実験は、我々のフレームワークがインスタンス固有のSBCから一般的な制約を学習できることを実証する。
  論文  参考訳（メタデータ） (2021-12-22T11:27:48Z)
• Coarsening Optimization for Differentiable Programming [8.204668529766256]
  粗い最適化は、象徴的分化とアルゴリズム的分化(AD)を相乗化するための体系的な方法を提供する 粗大化の象徴的分化に制御フローが生み出す困難を回避するため、この研究はフィカルキュラスを導入している。 実世界のアプリケーションの集合に関する実験では、粗大化最適化はADの高速化に有効であり、数倍から2桁のスピードアップを生み出すことが示されている。
  論文  参考訳（メタデータ） (2021-10-05T19:11:11Z)
• An Efficient Diagnosis Algorithm for Inconsistent Constraint Sets [68.8204255655161]
  過制約問題における最小限の障害制約を識別する分割・分散型診断アルゴリズム(FastDiag)を提案する。 ヒットセットの競合指向計算とfastdiagを比較し,詳細な性能解析を行う。
  論文  参考訳（メタデータ） (2021-02-17T19:55:42Z)
• ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system description) [0.4893345190925177]
  本稿では,飽和式自動定理証明器の勾配押し上げと神経誘導の実装について述べる。 勾配ブースティング法では、論理式のアリティに基づく符号化を考慮し、手動で抽象的な特徴を生成できる。 ニューラルネットワークでは,シンボルに依存しないグラフニューラルネットワーク(GNN)と,その用語や節の埋め込みを用いる。
  論文  参考訳（メタデータ） (2020-02-13T09:44:38Z)

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

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