Augmented Weak Distance for Fast and Accurate Bounds Checking
Zhoulai Fu, Freek Verbeek, Binoy Ravindran

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,…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsMachine Learning and Algorithms · Fault Detection and Control Systems · Formal Methods in Verification
