ESBMC v7.4: Harnessing the Power of Intervals

• URL: http://arxiv.org/abs/2312.14746v1
• Date: Fri, 22 Dec 2023 14:56:46 GMT
• Title: ESBMC v7.4: Harnessing the Power of Intervals
• Authors: Rafael Menezes, Mohannad Aldughaim, Bruno Farias, Xianzhiyu Li, Edoardo Manino, Fedor Shmarov, Kunjian Song, Franz Brau{\ss}e, Mikhail R. Gadelha, Norbert Tihanyi, Konstantin Korovin, Lucas C. Cordeiro
• Abstract summary: ESBMC implements many state-of-the-art techniques for model checking. New features allow us to obtain verification results for unsupported programs and properties. ESBMC employs a new interval analysis of expressions in programs to increase verification performance.
• Score: 4.6232063855710654
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: ESBMC implements many state-of-the-art techniques for model checking. We report on new and improved features that allow us to obtain verification results for previously unsupported programs and properties. ESBMC employs a new static interval analysis of expressions in programs to increase verification performance. This includes interval-based reasoning over booleans and integers, forward and backward contractors, and particular optimizations related to singleton intervals because of their ubiquity. Other relevant improvements concern the verification of concurrent programs, as well as several operational models, internal ones, and also those of libraries such as pthread and the C mathematics library. An extended memory safety analysis now allows tracking of memory leaks that are considered still reachable.

Related papers

• MOLA: Enhancing Industrial Process Monitoring Using Multi-Block Orthogonal Long Short-Term Memory Autoencoder [3.7028696448588487]
  We introduce MOLA: a Multi-block Orthogonal Long short-term memory Autoencoder paradigm, to conduct accurate, reliable fault detection of industrial processes. We propose a multi-block monitoring structure, which categorizes the process variables into multiple blocks by leveraging expert process knowledge. We demonstrate the efficiency and effectiveness of our MOLA framework by applying it to the Tennessee Eastman Process.
  arXiv  Detail & Related papers  (2024-10-10T00:49:43Z)
• OCTrack: Benchmarking the Open-Corpus Multi-Object Tracking [63.53176412315835]
  We study a novel yet practical problem of open-corpus multi-object tracking (OCMOT) We build OCTrackB, a large-scale and comprehensive benchmark, to provide a standard evaluation platform for the OCMOT problem.
  arXiv  Detail & Related papers  (2024-07-19T05:58:01Z)
• Interval Analysis in Industrial-Scale BMC Software Verifiers: A Case Study [4.024189528766689]
  We evaluate whether the computational cost of interval analysis yields significant enough improvements in BMC's performance to justify its use. Our results show that interval analysis is essential in solving 203 unique benchmarks.
  arXiv  Detail & Related papers  (2024-06-21T16:18:57Z)
• Temporally Consistent Referring Video Object Segmentation with Hybrid Memory [98.80249255577304]
  We propose an end-to-end R-VOS paradigm that explicitly models temporal consistency alongside the referring segmentation. Features of frames with automatically generated high-quality reference masks are propagated to segment remaining frames. Extensive experiments demonstrate that our approach enhances temporal consistency by a significant margin.
  arXiv  Detail & Related papers  (2024-03-28T13:32:49Z)
• Multi-grained Temporal Prototype Learning for Few-shot Video Object Segmentation [156.4142424784322]
  Few-Shot Video Object (FSVOS) aims to segment objects in a query video with the same category defined by a few annotated support images. We propose to leverage multi-grained temporal guidance information for handling the temporal correlation nature of video data. Our proposed video IPMT model significantly outperforms previous models on two benchmark datasets.
  arXiv  Detail & Related papers  (2023-09-20T09:16:34Z)
• Joint Modeling of Feature, Correspondence, and a Compressed Memory for Video Object Segmentation [52.11279360934703]
  Current prevailing Video Object (VOS) methods usually perform dense matching between the current and reference frames after extracting features. We propose a unified VOS framework, coined as JointFormer, for joint modeling of the three elements of feature, correspondence, and a compressed memory.
  arXiv  Detail & Related papers  (2023-08-25T17:30:08Z)
• A New Era in Software Security: Towards Self-Healing Software via Large Language Models and Formal Verification [8.733354577147093]
  This paper introduces an innovative approach that combines Large Language Models (LLMs) with Formal Verification strategies for automatic software vulnerability repair. We present the ESBMC-AI framework as a proof of concept, leveraging the well-recognized and industry-adopted Efficient SMT-based Context-Bounded Model Checker (ESBMC) and a pre-trained transformer model. Our results demonstrate ESBMC-AI's capability to automate the detection and repair of issues such as buffer overflow, arithmetic overflow, and pointer dereference failures with high accuracy.
  arXiv  Detail & Related papers  (2023-05-24T05:54:10Z)
• Joint Feature Learning and Relation Modeling for Tracking: A One-Stream Framework [76.70603443624012]
  We propose a novel one-stream tracking (OSTrack) framework that unifies feature learning and relation modeling. In this way, discriminative target-oriented features can be dynamically extracted by mutual guidance. OSTrack achieves state-of-the-art performance on multiple benchmarks, in particular, it shows impressive results on the one-shot tracking benchmark GOT-10k.
  arXiv  Detail & Related papers  (2022-03-22T18:37:11Z)
• Algorithm to Compilation Co-design: An Integrated View of Neural Network Sparsity [0.8566457170664925]
  We apply structured and unstructured pruning to attention weights of transformer blocks of the BERT language model. We study relationships between modeling decisions and their direct impact on sparsity-enhanced execution.
  arXiv  Detail & Related papers  (2021-06-16T15:13:26Z)
• Online Multiple Object Tracking with Cross-Task Synergy [120.70085565030628]
  We propose a novel unified model with synergy between position prediction and embedding association. The two tasks are linked by temporal-aware target attention and distractor attention, as well as identity-aware memory aggregation model.
  arXiv  Detail & Related papers  (2021-04-01T10:19:40Z)
• GRAPHSPY: Fused Program Semantic-Level Embedding via Graph Neural Networks for Dead Store Detection [4.82596017481926]
  We propose a learning-grained approach to identify unnecessary memory operations intelligently with low overhead. By applying several prevalent graph neural network models to extract program semantics, we present a novel, hybrid program embedding approach. Results show that our model achieves 90% of accuracy and incurs only around a half of time overhead of the state-of-art tool.
  arXiv  Detail & Related papers  (2020-11-18T19:17:15Z)

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.