論文の概要: Divide, Conquer and Verify: Improving Symbolic Execution Performance

• arxiv url: http://arxiv.org/abs/2310.03598v2
• Date: Tue, 7 Nov 2023 09:51:41 GMT
• ステータス: 処理完了
• システム内更新日: 2024-03-19 03:12:08.762581
• Title: Divide, Conquer and Verify: Improving Symbolic Execution Performance
• Title（参考訳）: Divide, Conquer and Verify: シンボリックな実行パフォーマンスの向上
• Authors: Christopher Scherb, Luc Bryan Heitz, Hermann Grieder, Olivier Mattmann,
• Abstract要約: シンボル実行(英: Symbolic Execution)は、コンピュータプログラムの動作を確認し、ソフトウェア脆弱性を検出するための形式的な方法である。 近年のパフォーマンス向上にもかかわらず、Symbolic Executionは現実のソフトウェアに適用するには遅すぎる。 個別のスライスを実行し,その後に副作用を組み合わせることで,シンボル実行のための分割・コンカレント手法を提案する。
• 参考スコア（独自算出の注目度）: 0.14999444543328289
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Symbolic Execution is a formal method that can be used to verify the behavior of computer programs and detect software vulnerabilities. Compared to other testing methods such as fuzzing, Symbolic Execution has the advantage of providing formal guarantees about the program. However, despite advances in performance in recent years, Symbolic Execution is too slow to be applied to real-world software. This is primarily caused by the \emph{path explosion problem} as well as by the computational complexity of SMT solving. In this paper, we present a divide-and-conquer approach for symbolic execution by executing individual slices and later combining the side effects. This way, the overall problem size is kept small, reducing the impact of computational complexity on large problems.
• Abstract（参考訳）: シンボル実行(英: Symbolic Execution)は、コンピュータプログラムの動作を確認し、ソフトウェア脆弱性を検出するための形式的な方法である。 ファジィングのような他のテスト手法と比較して、シンボリック実行はプログラムに関する正式な保証を提供するという利点がある。 しかし、近年の性能向上にもかかわらず、シンボリック実行は現実のソフトウェアに適用するには遅すぎる。 これは主に \emph{path explosion problem} と SMT 解決の計算複雑性によって引き起こされる。 本稿では、個々のスライスを実行し、その後に副作用を組み合わせることで、シンボリック実行のための分割対コンカレントアプローチを提案する。 このように、全体的な問題のサイズは小さく保たれ、大きな問題に対する計算複雑性の影響が減少する。

関連論文リスト

• To CoT or not to CoT? Chain-of-thought helps mainly on math and symbolic reasoning [55.52872152909785]
  Chain-of-Thought (CoT) は,大規模言語モデル (LLM) から推論能力を引き出すデファクト手法である。 私たちは、CoTが主に数学や論理学を含むタスクに強いパフォーマンス上の利点をもたらし、他のタスクよりもはるかに少ない利益をもたらすことを示しています。
  論文  参考訳（メタデータ） (2024-09-18T17:55:00Z)
• Scaling Symbolic Execution to Large Software Systems [0.0]
  シンボル実行は、プログラム検証とバグ検出ソフトウェアの両方で使用される一般的な静的解析手法である。 我々は、Clang Static Analyzerと呼ばれるエラー検出フレームワークと、その周辺に構築されたインフラストラクチャーであるCodeCheckerに焦点を当てた。
  論文  参考訳（メタデータ） (2024-08-04T02:54:58Z)
• Path-optimal symbolic execution of heap-manipulating programs [5.639904484784126]
  本稿では、当初、ヒープ操作プログラムに対して経路最適性を実現するシンボル実行アルゴリズムであるPOSEについて紹介する。 我々は,POSEアルゴリズムを小型で汎用的なオブジェクト指向プログラミング言語に形式化し,プロトタイプのシンボルエグゼキュータに形式化を実装し,データ構造を入力とするサンプルプログラムのベンチマークに対して,アルゴリズムを実験する。
  論文  参考訳（メタデータ） (2024-07-23T20:35:33Z)
• Parsimonious Optimal Dynamic Partial Order Reduction [1.5029560229270196]
  本稿では,Parsimonious-Optimal DPOR(POP)を提案する。 POPは、(i)同じ人種の複数の逆転を避ける擬似的な人種反転戦略を含む、いくつかの新しいアルゴリズム技術を組み合わせている。 我々のNidhuggの実装は、これらの手法が並列プログラムの解析を著しく高速化し、メモリ消費を抑えられることを示している。
  論文  参考訳（メタデータ） (2024-05-18T00:07:26Z)
• NExT: Teaching Large Language Models to Reason about Code Execution [50.93581376646064]
  大規模言語モデル(LLM)のコードは通常、プログラムの表面テキスト形式に基づいて訓練される。 NExTは,プログラムの実行トレースを検査し,実行時の動作を判断する手法である。
  論文  参考訳（メタデータ） (2024-04-23T01:46:32Z)
• Holographic Global Convolutional Networks for Long-Range Prediction Tasks in Malware Detection [50.7263393517558]
  ホログラフィック還元表現(HRR)の特性を利用したホログラフィックグローバル畳み込みネットワーク(HGConv)を導入する。 他のグローバルな畳み込み法とは異なり、我々の手法は複雑なカーネル計算や人工カーネル設計を必要としない。 提案手法は,Microsoft Malware Classification Challenge, Drebin, EMBERのマルウェアベンチマークで新たなSOTA結果を得た。
  論文  参考訳（メタデータ） (2024-03-23T15:49:13Z)
• Parallel Program Analysis on Path Ranges [3.018638214344819]
  Ranged symbolic execution は、並列にパス範囲と呼ばれるプログラム部分でシンボリックな実行を実行する。 本稿では,プログラムを経路範囲に分割し,任意の解析を並列に行う検証手法を提案する。
  論文  参考訳（メタデータ） (2024-02-19T08:26:52Z)
• Code Prompting: a Neural Symbolic Method for Complex Reasoning in Large Language Models [74.95486528482327]
  コードプロンプト(code prompting)は、ゼロショットバージョンと少数ショットバージョンの両方を持ち、中間ステップとしてコードをトリガーするニューラルシンボルプロンプトである。 我々は,記号的推論と算術的推論を含む7つの広く使用されているベンチマーク実験を行った。
  論文  参考訳（メタデータ） (2023-05-29T15:14:09Z)
• NAPG: Non-Autoregressive Program Generation for Hybrid Tabular-Textual Question Answering [52.10214317661547]
  現在の数値推論法はプログラムシーケンスを自己回帰的にデコードする。 プログラム生成の精度は、デコードステップがエラー伝搬によって展開されるにつれて急激に低下する。 本稿では,非自己回帰型プログラム生成フレームワークを提案する。
  論文  参考訳（メタデータ） (2022-11-07T11:25:21Z)
• High-performance symbolic-numerics via multiple dispatch [52.77024349608834]
  Symbolics.jlは拡張可能なシンボルシステムで、動的多重ディスパッチを使用してドメインのニーズに応じて振る舞いを変更する。 実装に依存しないアクションでジェネリックapiを形式化することで、システムに最適化されたデータ構造を遡及的に追加できることを示します。 従来の用語書き換えシンプリファイアと電子グラフベースの用語書き換えシンプリファイアをスワップする機能を実証する。
  論文  参考訳（メタデータ） (2021-05-09T14:22:43Z)
• Benchmarking Symbolic Execution Using Constraint Problems -- Initial Results [6.961253535504978]
  シンボル実行はバグ発見とプログラムテストのための強力なテクニックである。 我々はCSPベンチマークをシンボル実行ツールの推論能力をテストするのに適したCプログラムに変換する。
  論文  参考訳（メタデータ） (2020-01-22T08:48:55Z)

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

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