A shallow dive into the depths of non-termination checking for C programs

• URL: http://arxiv.org/abs/2409.12985v1
• Date: Wed, 4 Sep 2024 22:47:46 GMT
• Title: A shallow dive into the depths of non-termination checking for C programs
• Authors: Ravindra Metta, Hrishikesh Karmarkar, Kumar Madhukar, R Venkatesh, Supratik Chakraborty, Samarjit Chakraborty,
• Abstract summary: Unintended Non-Termination (NT) is common in real-world software development. We propose a sound and efficient technique for NT checking that is also effective on realworld software. Our experiments on wide ranging software benchmarks show that the technique outperforms state-of-the-art NT checkers.
• Score: 3.4144415576897624
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Checking for Non-Termination (NT) of a given program P, i.e., determining if P has at least one non-terminating run, is an undecidable problem that continues to garner significant research attention. While unintended NT is common in real-world software development, even the best-performing tools for NT checking are often ineffective on real-world programs and sometimes incorrect due to unrealistic assumptions such as absence of overflows. To address this, we propose a sound and efficient technique for NT checking that is also effective on realworld software. Given P, we encode the NT property as an assertion inside each loop of P to check for recurrent states in that loop, up to a fixed unwinding depth, using a Bounded Model Checker. The unwinding depth is increased iteratively until either NT is found or a predefined limit is reached. Our experiments on wide ranging software benchmarks show that the technique outperforms state-of-the-art NT checkers

Related papers

• Clip-and-Verify: Linear Constraint-Driven Domain Clipping for Accelerating Neural Network Verification [9.733843486234878]
  State-of-the-art neural network (NN) verifiers demonstrate that applying the branch-and-bound (BaB) procedure with fast bounding techniques plays a key role in tackling many challenging verification properties.<n>We introduce the linear constraint-driven clipping framework, a class of scalable and efficient methods designed to enhance the efficacy of NN verifiers.
  arXiv  Detail & Related papers  (2025-12-11T19:59:37Z)
• EndWatch: A Practical Method for Detecting Non-Termination in Real-World Software [30.67959999716073]
  We propose a practical termination checking technique, called EndWatch, for detecting non-termination caused by infinite loops through testing. We introduce two methods to generate non-termination oracles based on checking state revisits. The non-termination oracles can be incorporated into testing tools to detect non-termination in large programs.
  arXiv  Detail & Related papers  (2023-12-06T08:13:30Z)
• On Pitfalls of Test-Time Adaptation [82.8392232222119]
  Test-Time Adaptation (TTA) has emerged as a promising approach for tackling the robustness challenge under distribution shifts. We present TTAB, a test-time adaptation benchmark that encompasses ten state-of-the-art algorithms, a diverse array of distribution shifts, and two evaluation protocols.
  arXiv  Detail & Related papers  (2023-06-06T09:35:29Z)
• Efficient Deep Reinforcement Learning Requires Regulating Overfitting [91.88004732618381]
  We show that high temporal-difference (TD) error on the validation set of transitions is the main culprit that severely affects the performance of deep RL algorithms. We show that a simple online model selection method that targets the validation TD error is effective across state-based DMC and Gym tasks.
  arXiv  Detail & Related papers  (2023-04-20T17:11:05Z)
• The #DNN-Verification Problem: Counting Unsafe Inputs for Deep Neural Networks [94.63547069706459]
  #DNN-Verification problem involves counting the number of input configurations of a DNN that result in a violation of a safety property. We propose a novel approach that returns the exact count of violations. We present experimental results on a set of safety-critical benchmarks.
  arXiv  Detail & Related papers  (2023-01-17T18:32:01Z)
• Sound and Complete Verification of Polynomial Networks [55.9260539566555]
  Polynomial Networks (PNs) have demonstrated promising performance on face and image recognition recently. Existing verification algorithms on ReLU neural networks (NNs) based on branch and bound (BaB) techniques cannot be trivially applied to PN verification. We devise a new bounding method, equipped with BaB for global convergence guarantees, called VPN.
  arXiv  Detail & Related papers  (2022-09-15T11:50:43Z)
• A Continual Deepfake Detection Benchmark: Dataset, Methods, and Essentials [97.69553832500547]
  This paper suggests a continual deepfake detection benchmark (CDDB) over a new collection of deepfakes from both known and unknown generative models. We exploit multiple approaches to adapt multiclass incremental learning methods, commonly used in the continual visual recognition, to the continual deepfake detection problem.
  arXiv  Detail & Related papers  (2022-05-11T13:07:19Z)
• Unsupervised Domain Adaptation: A Reality Check [23.79809492395849]
  We show via large-scale experimentation that the difference in accuracy between UDA algorithms is smaller than previously thought. This is despite the fact that validation methods are a crucial component of any UDA train/val pipeline.
  arXiv  Detail & Related papers  (2021-11-30T18:59:04Z)
• CURE: Code-Aware Neural Machine Translation for Automatic Program Repair [11.556110575946631]
  We propose CURE, a new NMT-based APR technique with three major novelties. CURE pre-trains a programming language (PL) model on a large software to learn developer-like source code before the APR task. Second, CURE designs a new code-aware search strategy that finds more correct fixes by focusing on compilable patches and patches that are close in length to the buggy code.
  arXiv  Detail & Related papers  (2021-02-26T22:30:28Z)
• A Lower Bound on DNNF Encodings of Pseudo-Boolean Constraints [3.42658286826597]
  Two major considerations when encoding pseudo-Boolean constraints into SAT are the size of the encoding and its propagation strength. It has been shown that there exist PB-constraints whose ordered BDD (OBDD) representations, and thus the inferred CNF encodings, all have exponential size.
  arXiv  Detail & Related papers  (2021-01-06T10:25:22Z)
• Global Optimization of Objective Functions Represented by ReLU Networks [77.55969359556032]
  Neural networks can learn complex, non- adversarial functions, and it is challenging to guarantee their correct behavior in safety-critical contexts. Many approaches exist to find failures in networks (e.g., adversarial examples), but these cannot guarantee the absence of failures. We propose an approach that integrates the optimization process into the verification procedure, achieving better performance than the naive approach.
  arXiv  Detail & Related papers  (2020-10-07T08:19:48Z)

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.