Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Augmented Weak Distance for Fast and Accurate Bounds Checking

Zhoulai Fu, Freek Verbeek, Binoy Ravindran

TL;DR

The paper tackles the challenge of verifying floating-point programs by extending the Weak-Distance framework into Augmented Weak-Distance (AWD). AWD adds a Monotonic Convergence Condition (MCC) and per-path optimization via path-input affinity, yielding a well-conditioned optimization landscape that effectively handles loops and external calls. Empirically, AWD achieves 100% accuracy on 40 SV-COMP 2024 bounds-check benchmarks, matching the state-of-the-art CBMC while delivering a 170× speedup on average, and outperforming Astrée in accuracy. The work provides a practical, solver-free approach to precise floating-point verification with strong correctness guarantees and significant runtime benefits, enabling scalable analysis across real-world programs.

Abstract

This work advances floating-point program verification by introducing Augmented Weak-Distance (AWD), a principled extension of the Weak-Distance (WD) framework. WD is a recent approach that reformulates program analysis as a numerical minimization problem, providing correctness guarantees through non-negativity and zero-target correspondence. It consistently outperforms traditional floating-point analysis, often achieving speedups of several orders of magnitude. However, WD suffers from ill-conditioned optimization landscapes and branching discontinuities, which significantly hinder its practical effectiveness. AWD overcomes these limitations with two key contributions. First, it enforces the Monotonic Convergence Condition (MCC), ensuring a strictly decreasing objective function and mitigating misleading optimization stalls. Second, it extends WD with a per-path analysis scheme, preserving the correctness guarantees of weak-distance theory while integrating execution paths into the optimization process. These enhancements construct a well-conditioned optimization landscape, enabling AWD to handle floating-point programs effectively, even in the presence of loops and external functions. We evaluate AWD on SV-COMP 2024, a widely used benchmark for software verification.Across 40 benchmarks initially selected for bounds checking, AWD achieves 100% accuracy, matching the state-of-the-art bounded model checker CBMC, one of the most widely used verification tools, while running 170X faster on average. In contrast, the static analysis tool Astrée, despite being fast, solves only 17.5% of the benchmarks. These results establish AWD as a highly efficient alternative to CBMC for bounds checking, delivering precise floating-point verification without compromising correctness.

Augmented Weak Distance for Fast and Accurate Bounds Checking

TL;DR

The paper tackles the challenge of verifying floating-point programs by extending the Weak-Distance framework into Augmented Weak-Distance (AWD). AWD adds a Monotonic Convergence Condition (MCC) and per-path optimization via path-input affinity, yielding a well-conditioned optimization landscape that effectively handles loops and external calls. Empirically, AWD achieves 100% accuracy on 40 SV-COMP 2024 bounds-check benchmarks, matching the state-of-the-art CBMC while delivering a 170× speedup on average, and outperforming Astrée in accuracy. The work provides a practical, solver-free approach to precise floating-point verification with strong correctness guarantees and significant runtime benefits, enabling scalable analysis across real-world programs.

Abstract

This work advances floating-point program verification by introducing Augmented Weak-Distance (AWD), a principled extension of the Weak-Distance (WD) framework. WD is a recent approach that reformulates program analysis as a numerical minimization problem, providing correctness guarantees through non-negativity and zero-target correspondence. It consistently outperforms traditional floating-point analysis, often achieving speedups of several orders of magnitude. However, WD suffers from ill-conditioned optimization landscapes and branching discontinuities, which significantly hinder its practical effectiveness. AWD overcomes these limitations with two key contributions. First, it enforces the Monotonic Convergence Condition (MCC), ensuring a strictly decreasing objective function and mitigating misleading optimization stalls. Second, it extends WD with a per-path analysis scheme, preserving the correctness guarantees of weak-distance theory while integrating execution paths into the optimization process. These enhancements construct a well-conditioned optimization landscape, enabling AWD to handle floating-point programs effectively, even in the presence of loops and external functions. We evaluate AWD on SV-COMP 2024, a widely used benchmark for software verification.Across 40 benchmarks initially selected for bounds checking, AWD achieves 100% accuracy, matching the state-of-the-art bounded model checker CBMC, one of the most widely used verification tools, while running 170X faster on average. In contrast, the static analysis tool Astrée, despite being fast, solves only 17.5% of the benchmarks. These results establish AWD as a highly efficient alternative to CBMC for bounds checking, delivering precise floating-point verification without compromising correctness.

Paper Structure

This paper contains 34 sections, 1 theorem, 11 equations, 4 figures, 1 table, 1 algorithm.

Table of Contents

  1. Introduction
  2. The Weak-Distance Approach
  3. Augmented Weak-Distance
  4. Empirical Results
  5. Weak Distance: Pitfalls and How We Address Them
  6. Example 1: Non-Monotonic Descent Disrupts Optimization
  7. How Weak Distance is Normally Applied
  8. Why Weak Distance Fails
  9. Fixing the Issue: Monotonic Convergence Condition (MCC)
  10. Example 2: Ignoring Per-Path Behavior Misses Solutions
  11. How Weak Distance is Normally Applied
  12. Why Weak Distance Fails
  13. Fixing the Issue: Per-Path Optimization
  14. Takeaways
  15. Foundations of Augmented Weak Distance
  16. ...and 19 more sections

Key Result

lemma 1

Let $(u_1, v_1)$ and $(u_2, v_2)$ be two pairs ordered lexicographically. Define the mapping $E(u, v) = uM + v$, where $M > \max(v)$ for all possible $v$. Then $E(u, v)$ preserves the lexicographic order:

Figures (4)

  • Figure 1: (a) A weak-distance for check_sum, and (b) its visualization
  • Figure 2: C Weak-Distance (L) and Augmented Weak-Distance (R) for check_sum.
  • Figure 3: Weak distance (L) and Augmented Weak Distance (R) for check_sum.
  • Figure 4: The fork branch and the $\mathtt{AWD}$ function.

Theorems & Definitions (4)

  • definition 1: Bounds Checking
  • definition 2: Path-Input Affinity
  • lemma 1
  • proof : Proof Sketch