Algorithmic Details behind the Predator Shape Analyser

• URL: http://arxiv.org/abs/2403.18491v1
• Date: Wed, 27 Mar 2024 12:05:49 GMT
• Title: Algorithmic Details behind the Predator Shape Analyser
• Authors: Kamil Dudka, Petr Muller, Petr Peringer, Veronika Šoková, Tomáš Vojnar,
• Abstract summary: This chapter concentrates on a detailed description of the algorithms behind the Predator shape analyser. Predator is particularly suited for formal analysis and verification of sequential non-recursive C code.
• Score: 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.

Related papers

• Scaling Laws for Embedding Dimension in Information Retrieval [26.21690287784803]
  We conduct a comprehensive analysis of the relationship between embedding dimension and retrieval performance.<n>We find that the scaling behavior fits a power law, allowing us to derive scaling laws for performance given only embedding dimension.<n>Our analysis shows that for evaluation tasks aligned with the training task, performance continues to improve as embedding size increases.
  arXiv  Detail & Related papers  (2026-02-04T21:27:12Z)
• Boosting Pointer Analysis With Large Language Model-Enhanced Allocation Function Detection [17.94389997355635]
  Existing approaches largely overlook custom allocators, leading to coarse aliasing and reduced analysis precision.<n>We present AFD, a novel technique that enhances pointer analysis by automatically identifying and modeling custom allocation functions.<n>We evaluate AFD on 15 real-world C projects, identifying over 600 custom AFs.
  arXiv  Detail & Related papers  (2025-09-26T16:08:58Z)
• Single-pass Adaptive Image Tokenization for Minimum Program Search [75.59409288259151]
  We propose a single-pass adaptive tokenizer, KARL, which predicts the appropriate number of tokens for an image in a single forward pass.<n> KARL matches the performance of recent adaptive tokenizers while operating in a single pass.
  arXiv  Detail & Related papers  (2025-07-10T17:59:53Z)
• CLIP Under the Microscope: A Fine-Grained Analysis of Multi-Object Representation [3.1667055223489786]
  Contrastive Language-Image Pre-training models excel in zero-shot classification, yet face challenges in complex multi-object scenarios. This study offers a comprehensive analysis of CLIP's limitations in these contexts using a specialized dataset, ComCO. Our findings reveal significant biases: the text encoder prioritizes first-mentioned objects, and the image encoder favors larger objects.
  arXiv  Detail & Related papers  (2025-02-27T07:34:42Z)
• Self-supervised Learning of Contextualized Local Visual Embeddings [0.0]
  Contextualized Local Visual Embeddings (CLoVE) is a self-supervised convolutional-based method that learns representations suited for dense prediction tasks. We benchmark CLoVE's pre-trained representations on multiple datasets. CLoVE reaches state-of-the-art performance for CNN-based architectures in 4 dense prediction downstream tasks.
  arXiv  Detail & Related papers  (2023-10-01T00:13:06Z)
• Recurrent Generic Contour-based Instance Segmentation with Progressive Learning [111.31166268300817]
  We propose a novel deep network architecture, i.e., PolySnake, for generic contour-based instance segmentation. Motivated by the classic Snake algorithm, the proposed PolySnake achieves superior and robust segmentation performance.
  arXiv  Detail & Related papers  (2023-01-21T05:34:29Z)
• Beyond the Prototype: Divide-and-conquer Proxies for Few-shot Segmentation [63.910211095033596]
  Few-shot segmentation aims to segment unseen-class objects given only a handful of densely labeled samples. We propose a simple yet versatile framework in the spirit of divide-and-conquer. Our proposed approach, named divide-and-conquer proxies (DCP), allows for the development of appropriate and reliable information.
  arXiv  Detail & Related papers  (2022-04-21T06:21:14Z)
• Assembly Planning from Observations under Physical Constraints [65.83676649042623]
  The proposed algorithm uses a simple combination of physical stability constraints, convex optimization and Monte Carlo tree search to plan assemblies. It is efficient and, most importantly, robust to the errors in object detection and pose estimation unavoidable in any real robotic system.
  arXiv  Detail & Related papers  (2022-04-20T16:51:07Z)
• TraSeTR: Track-to-Segment Transformer with Contrastive Query for Instance-level Instrument Segmentation in Robotic Surgery [60.439434751619736]
  We propose TraSeTR, a Track-to-Segment Transformer that exploits tracking cues to assist surgical instrument segmentation. TraSeTR jointly reasons about the instrument type, location, and identity with instance-level predictions. The effectiveness of our method is demonstrated with state-of-the-art instrument type segmentation results on three public datasets.
  arXiv  Detail & Related papers  (2022-02-17T05:52:18Z)
• Learning Dynamic Compact Memory Embedding for Deformable Visual Object Tracking [82.34356879078955]
  We propose a compact memory embedding to enhance the discrimination of the segmentation-based deformable visual tracking method. Our method outperforms the excellent segmentation-based trackers, i.e., D3S and SiamMask on DAVIS 2017 benchmark.
  arXiv  Detail & Related papers  (2021-11-23T03:07:12Z)
• Depth-aware Object Segmentation and Grasp Detection for Robotic Picking Tasks [13.337131101813934]
  We present a novel deep neural network architecture for joint class-agnostic object segmentation and grasp detection for robotic picking tasks. We introduce depth-aware Coordinate Convolution (CoordConv), a method to increase accuracy for point proposal based object instance segmentation. We evaluate the accuracy of grasp detection and instance segmentation on challenging robotic picking datasets, namely Sil'eane and OCID_grasp.
  arXiv  Detail & Related papers  (2021-11-22T11:06:33Z)
• Parallel and Multi-Objective Falsification with Scenic and VerifAI [11.152087017964584]
  We present extensions to the Scenic scenario specification language and VerifAI toolkit. We first present a parallelized framework that is interfaced with both the simulation and sampling capabilities of Scenic. We then present an extension of VerifAI's falsification algorithms to support multi-objective optimization during sampling.
  arXiv  Detail & Related papers  (2021-07-09T01:08:49Z)
• PalmTree: Learning an Assembly Language Model for Instruction Embedding [8.74990895782223]
  We propose to pre-train an assembly language model called PalmTree for generating general-purpose instruction embeddings. PalmTree has the best performance for intrinsic metrics, and outperforms the other instruction embedding schemes for all downstream tasks.
  arXiv  Detail & Related papers  (2021-01-21T22:30:01Z)
• A Trainable Optimal Transport Embedding for Feature Aggregation and its Relationship to Attention [96.77554122595578]
  We introduce a parametrized representation of fixed size, which embeds and then aggregates elements from a given input set according to the optimal transport plan between the set and a trainable reference. Our approach scales to large datasets and allows end-to-end training of the reference, while also providing a simple unsupervised learning mechanism with small computational cost.
  arXiv  Detail & Related papers  (2020-06-22T08:35:58Z)
• Retrograde Program Analysis: A Practical Tutorial [51.56484100374058]
  This tutorial condenses a longer exposition to a focused guide with definitions.<n>The aim is practical: short proofs, concrete invariants, and drop-in code and property tests.
  arXiv  Detail & Related papers  (2010-06-13T13:32:37Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.