論文の概要: Parallel Program Analysis on Path Ranges

• arxiv url: http://arxiv.org/abs/2402.11938v1
• Date: Mon, 19 Feb 2024 08:26:52 GMT
• ステータス: 処理完了
• システム内更新日: 2024-02-20 17:43:09.474710
• Title: Parallel Program Analysis on Path Ranges
• Title（参考訳）: 経路範囲の並列プログラム解析
• Authors: Jan Haltermanna, Marie-Christine Jakobs, Cedric Richter, Heike Wehrheim
• Abstract要約: Ranged symbolic execution は、並列にパス範囲と呼ばれるプログラム部分でシンボリックな実行を実行する。 本稿では,プログラムを経路範囲に分割し,任意の解析を並列に行う検証手法を提案する。
• 参考スコア（独自算出の注目度）: 3.2976453916809803
• License: http://creativecommons.org/licenses/by-sa/4.0/
• Abstract: Symbolic execution is a software verification technique symbolically running programs and thereby checking for bugs. Ranged symbolic execution performs symbolic execution on program parts, so called path ranges, in parallel. Due to the parallelism, verification is accelerated and hence scales to larger programs. In this paper, we discuss a generalization of ranged symbolic execution to arbitrary program analyses. More specifically, we present a verification approach that splits programs into path ranges and then runs arbitrary analyses on the ranges in parallel. Our approach in particular allows to run different analyses on different program parts. We have implemented this generalization on top of the tool CPAchecker and evaluated it on programs from the SV-COMP benchmark. Our evaluation shows that verification can benefit from the parallelisation of the verification task, but also needs a form of work stealing (between analyses) as to become efficient
• Abstract（参考訳）: シンボル実行は、プログラムを象徴的に実行し、バグをチェックするソフトウェア検証技法である。 Ranged symbolic execution は、並列にパス範囲と呼ばれるプログラム部分でシンボリックな実行を実行する。 並列性のため、検証は加速され、より大きなプログラムにスケールする。 本稿では,任意のプログラム解析に対する範囲付きシンボル実行の一般化について論じる。 具体的には,プログラムを経路範囲に分割し,任意の解析を並列に行う検証手法を提案する。 特に我々のアプローチは、異なるプログラムパーツで異なる分析を実行できる。 我々は,ツールCPAchecker上にこの一般化を実装し,SV-COMPベンチマークのプログラム上で評価した。 評価の結果, 検証作業の並列化は有効であるが, 効率的になるためには, 作業盗難(分析)の形式も必要であることがわかった。

関連論文リスト

• 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)
• Weakly Supervised Semantic Parsing with Execution-based Spurious Program Filtering [19.96076749160955]
  本稿では,プログラムの実行結果に基づくドメインに依存しないフィルタリング機構を提案する。 私たちはこれらの表現に対して多数決を行い、他のプログラムと大きく異なる意味を持つプログラムを特定し、フィルタリングします。
  論文  参考訳（メタデータ） (2023-11-02T11:45:40Z)
• Divide, Conquer and Verify: Improving Symbolic Execution Performance [0.14999444543328289]
  シンボル実行(英: Symbolic Execution)は、コンピュータプログラムの動作を確認し、ソフトウェア脆弱性を検出するための形式的な方法である。 近年のパフォーマンス向上にもかかわらず、Symbolic Executionは現実のソフトウェアに適用するには遅すぎる。 個別のスライスを実行し,その後に副作用を組み合わせることで,シンボル実行のための分割・コンカレント手法を提案する。
  論文  参考訳（メタデータ） (2023-10-05T15:21:10Z)
• Guess & Sketch: Language Model Guided Transpilation [59.02147255276078]
  学習されたトランスパイレーションは、手作業による書き直しやエンジニアリングの取り組みに代わるものだ。 確率的ニューラルネットワークモデル(LM)は、入力毎に可塑性出力を生成するが、正確性を保証するコストがかかる。 Guess & Sketch は LM の特徴からアライメントと信頼性情報を抽出し、意味的等価性を解決するためにシンボリック・ソルバに渡す。
  論文  参考訳（メタデータ） (2023-09-25T15:42:18Z)
• Improved Tree Search for Automatic Program Synthesis [91.3755431537592]
  重要な要素は、有効なプログラムの空間における効率的な探索を可能にすることである。 ここでは2つの大きな異なるDSL上でのアート結果の状態を導くMCTSの変種を提案する。
  論文  参考訳（メタデータ） (2023-03-13T15:09:52Z)
• QParallel: Explicit Parallelism for Programming Quantum Computers [62.10004571940546]
  並列量子プログラミングのための言語拡張を提案する。 QParallelは、現在の量子プログラミング言語における並列性に関する曖昧さを取り除く。 並列化によって最も利益を上げるサブルーチンを識別し,並列領域の配置にプログラマを誘導するツールを提案する。
  論文  参考訳（メタデータ） (2022-10-07T16:35:16Z)
• Learning from Self-Sampled Correct and Partially-Correct Programs [96.66452896657991]
  そこで本研究では,モデルが学習中にサンプリングを行い,自己サンプリングされた完全正当プログラムと部分正当プログラムの両方から学習することを提案する。 自己サンプリング型プログラムと部分修正型プログラムを併用することで,学習とサンプリングプロセスのガイドに役立てることができることを示す。 提案手法は,MLEを用いた単一の参照プログラムからの学習と比較して,パス@kの性能を3.1%から12.3%向上させる。
  論文  参考訳（メタデータ） (2022-05-28T03:31:07Z)
• Representing Partial Programs with Blended Abstract Semantics [62.20775388513027]
  プログラム合成エンジンにおける部分的なプログラム表現手法について紹介する。 モジュラーニューラルネットワークとして実装された近似実行モデルを学ぶ。 これらのハイブリッドニューロシンボリック表現は、実行誘導型シンセサイザーがより強力な言語構成を使うことができることを示す。
  論文  参考訳（メタデータ） (2020-12-23T20:40:18Z)
• Benchmarking Symbolic Execution Using Constraint Problems -- Initial Results [6.961253535504978]
  シンボル実行はバグ発見とプログラムテストのための強力なテクニックである。 我々はCSPベンチマークをシンボル実行ツールの推論能力をテストするのに適したCプログラムに変換する。
  論文  参考訳（メタデータ） (2020-01-22T08:48:55Z)

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

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