論文の概要: 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ベンチマークは、既存のシンボル実行ツールの限界を示すのに効果的です。
この取り組みの動機は、この形式のベンチマークが、シンボリック実行エンジンにおけるコア推論の改善の開発とエンジニアリングを促進することができると信じていることである。
関連論文リスト
- Parallel Program Analysis on Path Ranges [3.2976453916809803]
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) - Guess & Sketch: Language Model Guided Transpilation [61.24102712913847]
学習されたトランスパイレーションは、手作業による書き直しやエンジニアリングの取り組みに代わるものだ。
確率的ニューラルネットワークモデル(LM)は、入力毎に可塑性出力を生成するが、正確性を保証するコストがかかる。
Guess & Sketch は LM の特徴からアライメントと信頼性情報を抽出し、意味的等価性を解決するためにシンボリック・ソルバに渡す。
論文 参考訳(メタデータ) (2023-09-25T15:42:18Z) - 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) - HyperPUT: Generating Synthetic Faulty Programs to Challenge Bug-Finding
Tools [3.8520163964103835]
シードバグのあるプログラムを自動的に生成する補完的手法を提案する。
プログラム変換を漸進的に適用することで、"シード"バグからCプログラムを構築します。
論文 参考訳(メタデータ) (2022-09-14T13:09:41Z) - Benchmarking Constraint Inference in Inverse Reinforcement Learning [19.314352936252444]
多くの実世界の問題において、専門家が従う制約は、RLエージェントに数学的に、未知に指定することがしばしば困難である。
本稿では,ロボット制御と自律運転という2つの主要なアプリケーション領域の文脈において,CIRLベンチマークを構築する。
CIRLアルゴリズムのパフォーマンスを再現するための情報を含むこのベンチマークは、https://github.com/Guiliang/CIRL-benchmarks-publicで公開されている。
論文 参考訳(メタデータ) (2022-06-20T09:22:20Z) - Evolving Pareto-Optimal Actor-Critic Algorithms for Generalizability and
Stability [67.8426046908398]
汎用性と安定性は,実世界における強化学習(RL)エージェントの運用において重要な2つの目的である。
本稿では,アクター・クリティック・ロス関数の自動設計法であるMetaPGを提案する。
論文 参考訳(メタデータ) (2022-04-08T20:46:16Z) - 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) - Constraint-Handling Techniques for Particle Swarm Optimization
Algorithms [0.0]
人口ベースの手法は、従来の方法よりもはるかに複雑な問題を含む、さまざまな問題に対処することができる。
本研究の目的は,アルゴリズムに汎用的な設定を組み込んだPSOに適したCHTを開発し,比較することである。
論文 参考訳(メタデータ) (2021-01-25T01:49:10Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。