FPScan: An Automated Constraint-Based Analyzer for Floating-Point Anomaly Detection

• URL: http://arxiv.org/abs/2609.07492v1
• Date: Mon, 07 Sep 2026 13:41:01 GMT
• Title: FPScan: An Automated Constraint-Based Analyzer for Floating-Point Anomaly Detection
• Abstract summary: FPScan is a novel tool to formally define and detect catastrophic cancellation and absorption in floating-point programs.<n>Our approach starts with a custom static analyzer based on abstract interpretation to infer the order of magnitude of all program variables.<n>Off-the-shelf SMT solver is used to determine whether the program exhibits any of these critical numerical pitfalls.
• Score: 0.0
• License: http://creativecommons.org/licenses/by-nc-sa/4.0/
• Abstract: Writing error-free floating-point programs is a challenging task, especially for programmers who lack a strong background in numerical analysis and rounding-error propagation. State-of-the-art techniques typically aim to bound such errors using static or dynamic analysis. However, only a few tools explicitly address critical floating-point pitfalls such as absorption and catastrophic cancellation. These anomalies represent situations in which rounding errors are significantly amplified, causing the semantics of the finite-precision computation to deviate substantially from the real-number semantics. In this article, we present FPScan, a novel tool to formally define and detect both catastrophic cancellation and absorption in floating-point programs. Our approach starts with a custom static analyzer based on abstract interpretation to infer the order of magnitude of all program variables. This magnitude information is then used to build a set of first-order constraints that model error propagation and numerical precision within the program. Finally, we employ an off-the-shelf SMT solver to determine whether the program exhibits any of these critical numerical pitfalls. Experiments were conducted on FPBench, a well-known benchmark suite of floating-point programs, to evaluate the effectiveness of our tool. We also present a comparison with state-of-the-art tools regarding soundness and analysis time.

Related papers

• LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation [75.05397479715576]
  Large language models (LLMs) and agents have shown promising progress, but their true capabilities and failure modes remain unclear.<n>We present the first systematic and contamination-aware study of LLM- and agent-based formal specification generation for C programs.
  arXiv  Detail & Related papers  (2026-05-02T11:31:33Z)
• Revisiting Code Debloating with Ground Truth-based Evaluation [5.955975465516521]
  Program debloating aims to remove unused code to reduce performance overhead, attack surfaces, and maintenance costs.<n>Despite its central role, application-level debloating continues to rely on imperfect proxies for measuring performance.<n>We revisit the foundations of application-level debloating through a ground-truth-based evaluation paradigm.
  arXiv  Detail & Related papers  (2026-04-20T01:58:17Z)
• Dynamic analysis enhances issue resolution [53.50448142467294]
  DAIRA (Dynamic Analysis-enhanced Issue Resolution Agent) is an automated repair framework that embeds dynamic analysis into the agent's reasoning cycle.<n> Driven by a Test Tracing-Driven methodology, DAIRA utilizes lightweight monitors to extract critical runtime data.<n>When powered by Gemini 3 Flash Preview, DAIRA establishes a new state-of-the-art (SOTA) performance, achieving a 79.4% resolution rate on the SWE-bench Verified dataset.
  arXiv  Detail & Related papers  (2026-03-23T14:48:54Z)
• Computing Floating-Point Errors by Injecting Perturbations [10.580959733598519]
  Floating-point programs form the foundation of modern science and engineering.<n> floating-point errors widely exist, but only a subset of inputs may trigger significant errors in floating-point programs.<n>We propose PI-detector to computing floating-point errors effectively and efficiently.
  arXiv  Detail & Related papers  (2025-07-11T10:19:14Z)
• Understanding and Mitigating Numerical Sources of Nondeterminism in LLM Inference [31.2331188304598]
  Changing system configuration, such as evaluation batch size, GPU count, and GPU version, can introduce significant differences in the generated responses.<n>We trace the root cause of this variability to the non-associative nature of floating-point arithmetic under limited numerical precision.<n>Inspired by this, we develop a lightweight inference pipeline, dubbed LayerCast, that stores weights in 16-bit precision but performs all computations in FP32.
  arXiv  Detail & Related papers  (2025-06-11T08:23:53Z)
• Satire: Computing Rigorous Bounds for Floating-Point Rounding Error in Mixed-Precision Loop-Free Programs [0.0]
  Satire is a tool that allows designers to trade error-bound tightness for gains in analysis time.<n>satire can be used during the design of numerical routines to effect design tradeoffs guided by rigorous empirical error guarantees.
  arXiv  Detail & Related papers  (2025-03-07T20:46:38Z)
• Accelerated zero-order SGD under high-order smoothness and overparameterized regime [79.85163929026146]
  We present a novel gradient-free algorithm to solve convex optimization problems. Such problems are encountered in medicine, physics, and machine learning. We provide convergence guarantees for the proposed algorithm under both types of noise.
  arXiv  Detail & Related papers  (2024-11-21T10:26:17Z)
• An evaluation framework for dimensionality reduction through sectional curvature [59.40521061783166]
  In this work, we aim to introduce the first highly non-supervised dimensionality reduction performance metric. To test its feasibility, this metric has been used to evaluate the performance of the most commonly used dimension reduction algorithms. A new parameterized problem instance generator has been constructed in the form of a function generator.
  arXiv  Detail & Related papers  (2023-03-17T11:59:33Z)
• On the Convergence of Stochastic Gradient Descent in Low-precision Number Formats [3.408623772471354]
  The convergence of single-precision Gradient Descent (SGD) is normally aligned with the theoretical results of real numbers. However, the numerical error increases when the computations are performed in low-precision number formats. This provides compelling reasons to study the SGD convergence adapted for low-precision computations.
  arXiv  Detail & Related papers  (2023-01-04T14:54:15Z)
• Deep Subspace Encoders for Nonlinear System Identification [0.0]
  We propose a method which uses a truncated prediction loss and a subspace encoder for state estimation. We show that, under mild conditions, the proposed method is locally consistent, increases optimization stability, and achieves increased data efficiency.
  arXiv  Detail & Related papers  (2022-10-26T16:04:38Z)
• 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)
• Bias-Variance Tradeoffs in Single-Sample Binary Gradient Estimators [100.58924375509659]
  Straight-through (ST) estimator gained popularity due to its simplicity and efficiency. Several techniques were proposed to improve over ST while keeping the same low computational complexity. We conduct a theoretical analysis of Bias and Variance of these methods in order to understand tradeoffs and verify originally claimed properties.
  arXiv  Detail & Related papers  (2021-10-07T15:16:07Z)

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.