論文の概要: Benchmarking Symbolic Execution Using Constraint Problems -- Initial Results

• arxiv url: http://arxiv.org/abs/2001.07914v1
• Date: Wed, 22 Jan 2020 08:48:55 GMT
• ステータス: 処理完了
• システム内更新日: 2023-01-07 18:48:56.748544
• Title: Benchmarking Symbolic Execution Using Constraint Problems -- Initial Results
• Title（参考訳）: 制約問題を用いたシンボリック実行のベンチマーク -- 初期結果
• Authors: Sahil Verma, Roland H.C. Yap
• Abstract要約: シンボル実行はバグ発見とプログラムテストのための強力なテクニックである。 我々はCSPベンチマークをシンボル実行ツールの推論能力をテストするのに適したCプログラムに変換する。
• 参考スコア（独自算出の注目度）: 6.961253535504978
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Symbolic execution is a powerful technique for bug finding and program testing. It is successful in finding bugs in real-world code. The core reasoning techniques use constraint solving, path exploration, and search, which are also the same techniques used in solving combinatorial problems, e.g., finite-domain constraint satisfaction problems (CSPs). We propose CSP instances as more challenging benchmarks to evaluate the effectiveness of the core techniques in symbolic execution. We transform CSP benchmarks into C programs suitable for testing the reasoning capabilities of symbolic execution tools. From a single CSP P, we transform P depending on transformation choice into different C programs. Preliminary testing with the KLEE, Tracer-X, and LLBMC tools show substantial runtime differences from transformation and solver choice. Our C benchmarks are effective in showing the limitations of existing symbolic execution tools. The motivation for this work is we believe that benchmarks of this form can spur the development and engineering of improved core reasoning in symbolic execution engines.
• Abstract（参考訳）: シンボル実行はバグ発見とプログラムテストのための強力なテクニックである。 現実世界のコードにバグを見つけることに成功している。 中心となる推論技術は制約解法、経路探索法、探索法を用いており、これは組合せ問題、例えば有限領域制約満足度問題(英語版)(csps)の解法と同じ手法である。 シンボリック実行におけるコア技術の有効性を評価するために,より困難なベンチマークとしてCSPインスタンスを提案する。 我々はCSPベンチマークをシンボル実行ツールの推論能力をテストするのに適したCプログラムに変換する。 1つの CSP P から、変換の選択によって P を異なる C プログラムに変換する。 klee、tracer-x、llbmcツールによる予備テストでは、トランスフォーメーションとソルバの選択とは大きく異なる。 我々のCベンチマークは、既存のシンボル実行ツールの限界を示すのに効果的です。 この取り組みの動機は、この形式のベンチマークが、シンボリック実行エンジンにおけるコア推論の改善の開発とエンジニアリングを促進することができると信じていることである。

関連論文リスト

• 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)
• DOCE: Finding the Sweet Spot for Execution-Based Code Generation [69.5305729627198]
  本稿では,候補生成,$n$-best再ランク,最小ベイズリスク(MBR)復号化,自己老化などを含む包括的フレームワークを提案する。 本研究は,実行ベースメソッドの重要性と,実行ベースメソッドと実行フリーメソッドとの差を明らかにする。
  論文  参考訳（メタデータ） (2024-08-25T07:10:36Z)
• SEPE-SQED: Symbolic Quick Error Detection by Semantically Equivalent Program Execution [34.48913676566932]
  シンボリッククイックエラー検出(SQED)は、フォーマルチップ検証の効率を大幅に改善した。 意味的に等価なプログラム実行(SEPE-SQED)による記号的クイックエラー検出という新しい変種を提案する。 SEPE-SQEDは、元の命令とその意味論的に等価なプログラムに対する影響を識別することにより、単一命令バグを効果的に検出する。
  論文  参考訳（メタデータ） (2024-04-04T03:11:24Z)
• Parallel Program Analysis on Path Ranges [3.018638214344819]
  Ranged symbolic execution は、並列にパス範囲と呼ばれるプログラム部分でシンボリックな実行を実行する。 本稿では,プログラムを経路範囲に分割し,任意の解析を並列に行う検証手法を提案する。
  論文  参考訳（メタデータ） (2024-02-19T08:26:52Z)
• Quantum Algorithm Exploration using Application-Oriented Performance Benchmarks [0.0]
  Application-Oriented BenchmarksのQED-Cスイートは、量子コンピュータの性能特性を測定する機能を提供する。 我々は,このベンチマーク手法がより複雑なアプリケーションに適用される可能性を広げる上での課題について検討する。
  論文  参考訳（メタデータ） (2024-02-14T06:55:50Z)
• Divide, Conquer and Verify: Improving Symbolic Execution Performance [0.14999444543328289]
  シンボル実行(英: Symbolic Execution)は、コンピュータプログラムの動作を確認し、ソフトウェア脆弱性を検出するための形式的な方法である。 近年のパフォーマンス向上にもかかわらず、Symbolic Executionは現実のソフトウェアに適用するには遅すぎる。 個別のスライスを実行し,その後に副作用を組み合わせることで,シンボル実行のための分割・コンカレント手法を提案する。
  論文  参考訳（メタデータ） (2023-10-05T15:21:10Z)
• Evaluating and Improving Tool-Augmented Computation-Intensive Math Reasoning [75.74103236299477]
  CoT(Chain-of- Thought prompting)とツール拡張は、大きな言語モデルを改善するための効果的なプラクティスとして検証されている。 ツールインターフェース,すなわち textbfDELI を用いた推論ステップを考慮に入れた新しい手法を提案する。 CARPと他の6つのデータセットの実験結果から、提案されたDELIは、主に競合ベースラインを上回っていることが示された。
  論文  参考訳（メタデータ） (2023-06-04T17:02:59Z)
• COPS: Controlled Pruning Before Training Starts [68.8204255655161]
  最先端のディープニューラルネットワーク(DNN)プルーニング技術は、トレーニング開始前にワンショットで適用され、プルーニングスコアと呼ばれる単一の基準の助けを借りてスパースアーキテクチャを評価する。 この作業では、単一プルーニング基準に集中するのではなく、任意のGASを組み合わせてより強力なプルーニング戦略を構築するためのフレームワークを提供します。
  論文  参考訳（メタデータ） (2021-07-27T08:48:01Z)
• Performance Evaluation of Adversarial Attacks: Discrepancies and Solutions [51.8695223602729]
  機械学習モデルの堅牢性に挑戦するために、敵対攻撃方法が開発されました。 本稿では,Piece-wise Sampling Curving(PSC)ツールキットを提案する。 psc toolkitは計算コストと評価効率のバランスをとるオプションを提供する。
  論文  参考訳（メタデータ） (2021-04-22T14:36:51Z)
• CoCoMoT: Conformance Checking of Multi-Perspective Processes via SMT (Extended Version) [62.96267257163426]
  我々はCoCoMoT(Computing Conformance Modulo Theories)フレームワークを紹介する。 まず、純粋な制御フロー設定で研究したSATベースのエンコーディングを、データ認識ケースに持ち上げる方法を示す。 次に,プロパティ保存型クラスタリングの概念に基づく新しい前処理手法を提案する。
  論文  参考訳（メタデータ） (2021-03-18T20:22:50Z)

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

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