A Formally Verified IEEE 754 Floating-Point Implementation of Interval Iteration for MDPs
Bram Kohlen, Maximilian Schäffeler, Mohammad Abdulaziz, Arnd Hartmanns, Peter Lammich
TL;DR
The paper tackles the challenge of obtaining correct-by-construction probabilistic model-checking results for MDPs under floating-point arithmetic. It presents a formally verified interval-iteration algorithm implemented via a refinement chain from abstract specifications in Isabelle/HOL to LLVM code, using the Isabelle Refinement Framework and directed rounding. The contributions include machine-checked proofs of convergence and bound preservation, a floating-point extension for FP reasoning, and an integration that yields competitive performance with state-of-the-art unverified tools while providing formal guarantees. This work advances a practical, fully verified PMC pipeline by bridging formal methods with high-performance verification tooling and sets the stage for verified backends for MEC decomposition and beyond.
Abstract
We present an efficiently executable, formally verified implementation of interval iteration for MDPs. Our correctness proofs span the entire development from the high-level abstract semantics of MDPs to a low-level implementation in LLVM that is based on floating-point arithmetic. We use the Isabelle/HOL proof assistant to verify convergence of our abstract definition of interval iteration and employ step-wise refinement to derive an efficient implementation in LLVM code. To that end, we extend the Isabelle Refinement Framework with support for reasoning about floating-point arithmetic and directed rounding modes. We experimentally demonstrate that the verified implementation is competitive with state-of-the-art tools for MDPs, while providing formal guarantees on the correctness of the results.