Verifying Floating-Point Programs in Stainless

TL;DR

The paper tackles the challenge of verifying floating-point programs in a real-world language by extending Stainless with bit-accurate FP reasoning for a Scala subset, following the axiomatic approach used by KeY and verifying those axioms against Stainless' implementation. It adds the Bitwuzla backend, a verified standard math library, automated NaN and cast-safety checks, and a large empirical evaluation on KeY benchmarks and GitHub-derived FP code, achieving verification or counterexamples in the majority of cases. Key findings include strong practical FP verification capability (about $82\%$ on empirical benchmarks), notable improvements for transcendental reasoning via the math library axioms, and effective detection of FP-related bugs through automated NaN checks. The work demonstrates the viability of scalable, automated FP verification for Scala programs with advanced features, while also identifying ongoing challenges in transcendental reasoning and solver performance that guide future enhancements and usability improvements.

Abstract

We extend the Stainless deductive verifier with floating-point support, providing the first automated verification support for floating-point numbers for a subset of Scala that includes polymorphism, recursion and higher-order functions. We follow the recent approach in the KeY verifier to axiomatise reasoning about mathematical functions, but go further by supporting all functions from Scala's math API, and by verifying the correctness of the axioms against the actual implementation in Stainless itself. We validate Stainless' floating-point support on a new set of benchmarks sampled from real-world code from GitHub, showing that it can verify specifications about, e.g., ranges of output or absence of special values for most supported functions, or produce counter-examples when the specifications do not hold.

Figures (6)

• Figure 1: Example floating-point programs extracted from GitHub
• Figure 2: Simplified architecture of Stainless
• Figure 3: Overview of the methodology to extract benchmarks from GitHub
• Figure 4: Solver runtime for verification conditions supported by all solvers
• Figure 6: Solver runtime for all verification conditions