SEPE-SQED: Symbolic Quick Error Detection by Semantically Equivalent Program Execution

• URL: http://arxiv.org/abs/2404.03172v2
• Date: Sat, 6 Apr 2024 07:55:11 GMT
• Title: SEPE-SQED: Symbolic Quick Error Detection by Semantically Equivalent Program Execution
• Authors: Yufeng Li, Qiusong Yang, Yiwei Ci, Enyuan Tian,
• Abstract summary: Symbolic quick error detection (SQED) has greatly improved efficiency in formal chip verification. We propose a new variant called symbolic quick error detection by semantically equivalent program execution (SEPE-SQED) SEPE-SQED effectively detects single-instruction bugs by differentiating their impact on the original instruction and its semantically equivalent program.
• Score: 34.48913676566932
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Symbolic quick error detection (SQED) has greatly improved efficiency in formal chip verification. However, it has a limitation in detecting single-instruction bugs due to its reliance on the self-consistency property. To address this, we propose a new variant called symbolic quick error detection by semantically equivalent program execution (SEPE-SQED), which utilizes program synthesis techniques to find sequences with equivalent meanings to original instructions. SEPE-SQED effectively detects single-instruction bugs by differentiating their impact on the original instruction and its semantically equivalent program (instruction sequence). To manage the search space associated with program synthesis, we introduce the CEGIS based on the highest priority first algorithm. The experimental results show that our proposed CEGIS approach improves the speed of generating the desired set of equivalent programs by 50% in time compared to previous methods. Compared to SQED, SEPE-SQED offers a wider variety of instruction combinations and can provide a shorter trace for triggering bugs in certain scenarios.

Related papers

• Inductive Predicate Synthesis Modulo Programs (Extended) [1.7372615815088566]
  A growing trend in program analysis is to encode verification conditions within the language of the input program. We propose Inductive Predicate Synthesis Modulo Programs (IPS-MP) which extends high-level languages with minimal synthesis features.
  arXiv  Detail & Related papers  (2024-07-11T12:51:08Z)
• Quantum Algorithm Exploration using Application-Oriented Performance Benchmarks [0.0]
  The QED-C suite of Application-Oriented Benchmarks provides the ability to gauge performance characteristics of quantum computers. We investigate challenges in broadening the relevance of this benchmarking methodology to applications of greater complexity.
  arXiv  Detail & Related papers  (2024-02-14T06:55:50Z)
• ASAG: Building Strong One-Decoder-Layer Sparse Detectors via Adaptive Sparse Anchor Generation [50.01244854344167]
  We bridge the performance gap between sparse and dense detectors by proposing Adaptive Sparse Anchor Generator (ASAG) ASAG predicts dynamic anchors on patches rather than grids in a sparse way so that it alleviates the feature conflict problem. Our method outperforms dense-d ones and achieves a better speed-accuracy trade-off.
  arXiv  Detail & Related papers  (2023-08-18T02:06:49Z)
• Fully Autonomous Programming with Large Language Models [0.9558392439655015]
  Current approaches to program synthesis with Large Language Models (LLMs) exhibit a "near miss syndrome" We use OpenAI Codex as the LLM and Program Synthesis Benchmark 2 as a database of problem descriptions and tests for evaluation. The resulting framework outperforms both conventional usage of Codex without the repair phase and traditional genetic programming approaches.
  arXiv  Detail & Related papers  (2023-04-20T16:12:05Z)
• A Stable, Fast, and Fully Automatic Learning Algorithm for Predictive Coding Networks [65.34977803841007]
  Predictive coding networks are neuroscience-inspired models with roots in both Bayesian statistics and neuroscience. We show how by simply changing the temporal scheduling of the update rule for the synaptic weights leads to an algorithm that is much more efficient and stable than the original one.
  arXiv  Detail & Related papers  (2022-11-16T00:11:04Z)
• Mitigating the Mutual Error Amplification for Semi-Supervised Object Detection [92.52505195585925]
  We propose a Cross Teaching (CT) method, aiming to mitigate the mutual error amplification by introducing a rectification mechanism of pseudo labels. In contrast to existing mutual teaching methods that directly treat predictions from other detectors as pseudo labels, we propose the Label Rectification Module (LRM)
  arXiv  Detail & Related papers  (2022-01-26T03:34:57Z)
• AP-Loss for Accurate One-Stage Object Detection [49.13608882885456]
  One-stage object detectors are trained by optimizing classification-loss and localization-loss simultaneously. The former suffers much from extreme foreground-background imbalance due to the large number of anchors. This paper proposes a novel framework to replace the classification task in one-stage detectors with a ranking task.
  arXiv  Detail & Related papers  (2020-08-17T13:22:01Z)
• Accelerated Message Passing for Entropy-Regularized MAP Inference [89.15658822319928]
  Maximum a posteriori (MAP) inference in discrete-valued random fields is a fundamental problem in machine learning. Due to the difficulty of this problem, linear programming (LP) relaxations are commonly used to derive specialized message passing algorithms. We present randomized methods for accelerating these algorithms by leveraging techniques that underlie classical accelerated gradient.
  arXiv  Detail & Related papers  (2020-07-01T18:43:32Z)
• ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system description) [0.4893345190925177]
  We describe an implementation of gradient boosting and neural guidance of saturation-style automated theorem provers. For the gradient-boosting guidance, we manually create abstracted features by considering arity-based encodings of formulas. For the neural guidance, we use symbol-independent graph neural networks (GNNs) and their embedding of the terms and clauses.
  arXiv  Detail & Related papers  (2020-02-13T09:44:38Z)

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.