論文の概要: Algorithmic Details behind the Predator Shape Analyser
- arxiv url: http://arxiv.org/abs/2403.18491v1
- Date: Wed, 27 Mar 2024 12:05:49 GMT
- ステータス: 処理完了
- システム内更新日: 2024-03-28 17:08:03.957677
- Title: Algorithmic Details behind the Predator Shape Analyser
- Title(参考訳): 捕食者形状解析装置のアルゴリズム的詳細
- Authors: Kamil Dudka, Petr Muller, Petr Peringer, Veronika Šoková, Tomáš Vojnar,
- Abstract要約: この章では、プレデター形状分析装置の背後にあるアルゴリズムの詳細な記述に焦点を当てている。
Predatorは、シーケンシャルな非再帰的なCコードの形式解析と検証に特に適している。
- 参考スコア(独自算出の注目度): 0.0
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: This chapter, which is an extended and revised version of the conference paper 'Predator: Byte-Precise Verification of Low-Level List Manipulation', concentrates on a detailed description of the algorithms behind the Predator shape analyser based on abstract interpretation and symbolic memory graphs. Predator is particularly suited for formal analysis and verification of sequential non-recursive C code that uses low-level pointer operations to manipulate various kinds of linked lists of unbounded size as well as various other kinds of pointer structures of bounded size. The tool supports practically relevant forms of pointer arithmetic, block operations, address alignment, or memory reinterpretation. We present the overall architecture of the tool, along with selected implementation details of the tool as well as its extension into so-called Predator Hunting Party, which utilises multiple concurrently-running Predator analysers with various restrictions on their behaviour. Results of experiments with Predator within the SV-COMP competition as well as on our own benchmarks are provided.
- Abstract(参考訳): 本章は,論文「Predator: Byte-Precise Verification of Low-Level List Manipulation」の改訂版であり,抽象的解釈とシンボリックメモリグラフに基づいて,プレデター形状解析の背景にあるアルゴリズムの詳細な記述に焦点を当てている。
プレデターは、低レベルのポインタ演算を用いて、非有界サイズの様々なリンクリストや、その他の有界サイズのポインタ構造を操作するシーケンシャルな非再帰的Cコードの形式解析と検証に特に適している。
このツールは、ポインタ演算、ブロック演算、アドレスアライメント、メモリ再解釈など、実質的に関連する形式をサポートしている。
ツールの全体的なアーキテクチャと、ツールの実装詳細、および、その動作に様々な制約を課した複数の同時実行型Predatorアナライザを活用した、いわゆるPredator Hunting Partyへの拡張について述べる。
SV-COMPコンペティションにおけるPredatorの実験結果とベンチマーク結果について報告する。
関連論文リスト
- Self-supervised Learning of Contextualized Local Visual Embeddings [0.0]
Contextualized Local Visual Embeddings (CLoVE) は、密集した予測タスクに適した表現を学習する自己教師型畳み込み方式である。
CLoVEの事前訓練された表現を複数のデータセットでベンチマークする。
CLOVEは、CNNベースのアーキテクチャに対して、下流の4つの密集した予測タスクで最先端のパフォーマンスに達する。
論文 参考訳(メタデータ) (2023-10-01T00:13:06Z) - Recurrent Generic Contour-based Instance Segmentation with Progressive
Learning [111.31166268300817]
本稿では,一般的な輪郭型インスタンスセグメンテーションのための新しいディープネットワークアーキテクチャ,すなわちPolySnakeを提案する。
従来のSnakeアルゴリズムに動機付け,提案したPolySnakeはより優れた,堅牢なセグメンテーション性能を実現する。
論文 参考訳(メタデータ) (2023-01-21T05:34:29Z) - Beyond the Prototype: Divide-and-conquer Proxies for Few-shot
Segmentation [63.910211095033596]
少ないショットのセグメンテーションは、少数の濃密なラベル付けされたサンプルのみを与えられた、目に見えないクラスオブジェクトをセグメンテーションすることを目的としている。
分割・分散の精神において, 単純かつ多目的な枠組みを提案する。
提案手法は、DCP(disvision-and-conquer proxies)と呼ばれるもので、適切な信頼性のある情報の開発を可能にする。
論文 参考訳(メタデータ) (2022-04-21T06:21:14Z) - Assembly Planning from Observations under Physical Constraints [65.83676649042623]
提案アルゴリズムは, 物理安定性制約, 凸最適化, モンテカルロ木探索の簡単な組み合わせを用いて, 集合を計画する。
それは効率的で、最も重要なことは、オブジェクト検出のエラーに対して堅牢であり、実際のロボットシステムでは避けられないポーズ推定である。
論文 参考訳(メタデータ) (2022-04-20T16:51:07Z) - TraSeTR: Track-to-Segment Transformer with Contrastive Query for
Instance-level Instrument Segmentation in Robotic Surgery [60.439434751619736]
そこで我々は,TraSeTRを提案する。TraSeTR,TraSeTR,Trace-to-Segment Transformerは,手術器具のセグメンテーションを支援する。
TraSeTRは、機器の種類、位置、アイデンティティとインスタンスレベルの予測を共同で理由付けている。
提案手法の有効性を,3つの公開データセットに対して,最先端の計器型セグメンテーション結果を用いて実証した。
論文 参考訳(メタデータ) (2022-02-17T05:52:18Z) - Learning Dynamic Compact Memory Embedding for Deformable Visual Object
Tracking [82.34356879078955]
本稿では,セグメント化に基づく変形可能な視覚追跡手法の識別を強化するために,コンパクトなメモリ埋め込みを提案する。
DAVIS 2017ベンチマークでは,D3SやSiamMaskなどのセグメンテーションベースのトラッカーよりも優れている。
論文 参考訳(メタデータ) (2021-11-23T03:07:12Z) - Depth-aware Object Segmentation and Grasp Detection for Robotic Picking
Tasks [13.337131101813934]
本稿では,ロボットピッキングタスクの協調型クラス非依存オブジェクト分割と把握検出のための新しいディープニューラルネットワークアーキテクチャを提案する。
本稿では,ポイント提案に基づくオブジェクトインスタンスセグメンテーションの精度を高める手法であるDeep-Aware Coordinate Convolution(CoordConv)を紹介する。
我々は,Sil'eane と OCID_grasp という,難易度の高いロボットピッキングデータセットに対して,把握検出とインスタンスセグメンテーションの精度を評価する。
論文 参考訳(メタデータ) (2021-11-22T11:06:33Z) - Parallel and Multi-Objective Falsification with Scenic and VerifAI [11.152087017964584]
シナリオ仕様言語とVerifAIツールキットの拡張について述べる。
まず,Scanicのシミュレーションとサンプリング機能の両方にインタフェースを組み込んだ並列化フレームワークを提案する。
次に、サンプリング中の多目的最適化をサポートするために、VerifAIのファルシフィケーションアルゴリズムの拡張を示す。
論文 参考訳(メタデータ) (2021-07-09T01:08:49Z) - PalmTree: Learning an Assembly Language Model for Instruction Embedding [8.74990895782223]
汎用命令埋め込み生成のためのアセンブリ言語モデルであるPalmTreeの事前トレーニングを提案する。
PalmTreeは固有のメトリクスに対して最高のパフォーマンスを持ち、下流タスクの他の命令埋め込みスキームよりも優れています。
論文 参考訳(メタデータ) (2021-01-21T22:30:01Z) - A Trainable Optimal Transport Embedding for Feature Aggregation and its
Relationship to Attention [96.77554122595578]
固定サイズのパラメータ化表現を導入し、与えられた入力セットから、そのセットとトレーニング可能な参照の間の最適な輸送計画に従って要素を埋め込み、集約する。
我々のアプローチは大規模なデータセットにスケールし、参照のエンドツーエンドのトレーニングを可能にすると同時に、計算コストの少ない単純な教師なし学習メカニズムも提供する。
論文 参考訳(メタデータ) (2020-06-22T08:35:58Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。