Augmented Weak Distance for Fast and Accurate Bounds Checking

TL;DR

This paper introduces Augmented Weak-Distance (AWD), a novel extension of the Weak-Distance framework that improves floating-point program verification by ensuring better optimization landscapes, leading to faster and more accurate bounds checking.

Contribution

AWD extends the Weak-Distance framework with the Monotonic Convergence Condition and per-path analysis, significantly enhancing optimization stability and effectiveness in floating-point verification.

Findings

Achieves 100% accuracy on 40 benchmarks for bounds checking.

Runs 170 times faster than CBMC on average.

Outperforms static analysis tool Astrée in benchmark coverage.

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\'ee, 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.