論文の概要: Targeted Control-flow Transformations for Mitigating Path Explosion in Dynamic Symbolic Execution

• arxiv url: http://arxiv.org/abs/2308.01554v1
• Date: Thu, 3 Aug 2023 06:34:34 GMT
• ステータス: 処理完了
• システム内更新日: 2023-10-23 15:30:53.459807
• Title: Targeted Control-flow Transformations for Mitigating Path Explosion in Dynamic Symbolic Execution
• Title（参考訳）: 動的シンボリック実行における経路爆発緩和のための制御フロー変換
• Authors: Charitha Saumya, Rohan Gangaraju, Kirshanthan Sundararajah, Milind Kulkarni
• Abstract要約: 動的シンボリック実行(DSE)は、ターゲットプログラムが多くの条件分岐を持つ場合、経路の爆発的な問題に悩まされる。 本稿では,高コストなシンボル分岐を除去する非意味保存型コンパイラ手法を提案する。
• 参考スコア（独自算出の注目度）: 0.27309692684728615
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Dynamic symbolic execution (DSE) suffers from path explosion problem when the target program has many conditional branches. Classical approach for managing the path explosion problem is dynamic state merging. Dynamic state merging combines similar symbolic program states together to avoid the exponential growth of states in DSE. However, state merging still requires solver invocations at each branch point of the program even when both paths of the branch is feasible and, the best path search strategy for DSE may not create the best state merging opportunities. Some drawbacks of state merging can be mitigated by compile-time state merging i.e. branch elimination by converting control-flow into data-flow. In this paper, we propose a non-semantics preserving but failure-preserving compiler technique for removing expensive symbolic branches in a program to improve the scalability of DSE. We develop a framework for detecting spurious bugs that can be inserted by our transformation. Finally, we show that our transformation can significantly improve the performance of exhaustive DSE on variety of benchmarks and helps in achieving more coverage in a large real-world subjects within a limited time budget.
• Abstract（参考訳）: 動的シンボリック実行(DSE)は、ターゲットプログラムが多くの条件分岐を持つ場合、経路爆発問題に悩まされる。 経路爆発問題を管理する古典的なアプローチは動的状態マージである。 動的状態マージは、DSEにおける状態の指数的な成長を避けるために、同様の記号的プログラム状態を組み合わせる。 しかし、状態マージは、分岐の双方の経路が実現可能であり、DSEの最良の経路探索戦略が最良の状態マージ機会を創出しない場合でも、プログラムの各分岐点でのソルバ呼び出しを必要とする。 状態マージの欠点は、コンパイル時の状態マージ、すなわち制御フローをデータフローに変換することによってブランチの排除によって軽減できる。 本稿では,DSEのスケーラビリティを向上するプログラムにおいて,高コストなシンボル分岐を除去する非セマンティクス保存型,非セマンティクス保存型コンパイラ手法を提案する。 変換によって挿入できる急激なバグを検出するためのフレームワークを開発する。 最後に、我々の変換は、様々なベンチマークにおける徹底的なDSEの性能を大幅に向上させ、限られた時間予算で大規模な現実世界の被験者により多くのカバレッジを達成できることを示す。

関連論文リスト

• COrAL: Order-Agnostic Language Modeling for Efficient Iterative Refinement [80.18490952057125]
  反復改良は、複雑なタスクにおける大規模言語モデル(LLM)の能力を高める効果的なパラダイムとして登場した。 我々はこれらの課題を克服するために、コンテキストワイズ順序非依存言語モデリング(COrAL)を提案する。 当社のアプローチでは、管理可能なコンテキストウィンドウ内で複数のトークン依存関係をモデル化しています。
  論文  参考訳（メタデータ） (2024-10-12T23:56:19Z)
• Multi-Pass Targeted Dynamic Symbolic Execution [0.0]
  本稿では、ターゲットプログラム位置から始まり、特定のエントリポイントに到達するまで後退するマルチパスターゲット動的実行手法を提案する。 提案手法は,探索経路数の平均4倍の削減と2倍の高速化を実現する。
  論文  参考訳（メタデータ） (2024-08-14T20:14:59Z)
• Parsimonious Optimal Dynamic Partial Order Reduction [1.5029560229270196]
  本稿では,Parsimonious-Optimal DPOR(POP)を提案する。 POPは、(i)同じ人種の複数の逆転を避ける擬似的な人種反転戦略を含む、いくつかの新しいアルゴリズム技術を組み合わせている。 我々のNidhuggの実装は、これらの手法が並列プログラムの解析を著しく高速化し、メモリ消費を抑えられることを示している。
  論文  参考訳（メタデータ） (2024-05-18T00:07:26Z)
• Detecting Continuous Integration Skip : A Reinforcement Learning-based Approach [0.4297070083645049]
  継続的統合(CI)プラクティスは、自動ビルドとテストプロセスを採用することで、コード変更のシームレスな統合を促進する。 Travis CIやGitHub Actionsといった一部のフレームワークは、CIプロセスの簡素化と強化に大きく貢献している。 開発者はCI実行に適したコミットやスキップの候補としてコミットを正確にフラグ付けすることの難しさに悩まされ続けている。
  論文  参考訳（メタデータ） (2024-05-15T18:48:57Z)
• State Merging with Quantifiers in Symbolic Execution [1.07873286104678]
  状態統合時に導入された解離の数とif-then-else式を減らすことを目的としている。 主なアイデアは、シンボル状態が経路制約で検出された同様の一様構造に従って、動的に合併群に分割することである。
  論文  参考訳（メタデータ） (2023-08-23T11:29:20Z)
• Semantics-Aware Dynamic Localization and Refinement for Referring Image Segmentation [102.25240608024063]
  画像の参照は、言語表現からのイメージセグメントを参照する。 そこで我々は,局所化中心からセグメンテーション言語へ移行するアルゴリズムを開発した。 比較すると,本手法はより汎用的で有効である。
  論文  参考訳（メタデータ） (2023-03-11T08:42:40Z)
• Forward LTLf Synthesis: DPLL At Work [1.370633147306388]
  有限トレース(LTLf)上での線形時間論理の合成のための新しいAND-ORグラフ探索フレームワークを提案する。 このようなフレームワーク内では、Davis-Putnam-Logemann-Loveland (DPLL)アルゴリズムにインスパイアされたプロシージャを考案し、次に利用可能なエージェント環境の動きを生成する。 また,状態公式の構文的等価性に基づく探索ノードの等価性チェックも提案する。
  論文  参考訳（メタデータ） (2023-02-27T14:33:50Z)
• Near-optimal Policy Identification in Active Reinforcement Learning [84.27592560211909]
  AE-LSVI はカーネル化された最小二乗値 RL (LSVI) アルゴリズムの新しい変種であり、楽観主義と悲観主義を組み合わせて活発な探索を行う。 AE-LSVIは初期状態に対するロバスト性が必要な場合、様々な環境で他のアルゴリズムよりも優れていることを示す。
  論文  参考訳（メタデータ） (2022-12-19T14:46:57Z)
• Dynamic Convolution for 3D Point Cloud Instance Segmentation [146.7971476424351]
  動的畳み込みに基づく3次元点雲からのインスタンスセグメンテーション手法を提案する。 我々は、同じ意味圏と閉投票を持つ等質点を幾何学的遠近点に対して収集する。 提案手法は提案不要であり、代わりに各インスタンスの空間的および意味的特性に適応する畳み込みプロセスを利用する。
  論文  参考訳（メタデータ） (2021-07-18T09:05:16Z)
• High-performance symbolic-numerics via multiple dispatch [52.77024349608834]
  Symbolics.jlは拡張可能なシンボルシステムで、動的多重ディスパッチを使用してドメインのニーズに応じて振る舞いを変更する。 実装に依存しないアクションでジェネリックapiを形式化することで、システムに最適化されたデータ構造を遡及的に追加できることを示します。 従来の用語書き換えシンプリファイアと電子グラフベースの用語書き換えシンプリファイアをスワップする機能を実証する。
  論文  参考訳（メタデータ） (2021-05-09T14:22:43Z)
• ISTR: End-to-End Instance Segmentation with Transformers [147.14073165997846]
  ISTRと呼ばれるインスタンスセグメンテーショントランスフォーマーを提案します。これは、その種類の最初のエンドツーエンドフレームワークです。 ISTRは低次元マスクの埋め込みを予測し、それらのマスクの埋め込みと一致する。 ISTRは、提案されたエンドツーエンドのメカニズムにより、近似ベースのサブオプティマティック埋め込みでも最先端のパフォーマンスを発揮します。
  論文  参考訳（メタデータ） (2021-05-03T06:00:09Z)

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

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