A Formally Verified IEEE 754 Floating-Point Implementation of Interval Iteration for MDPs

Bram Kohlen, Maximilian Schäffeler, Mohammad Abdulaziz +2

We present an efficiently executable, formally verified implementation of interval iteration for MDPs. Our correctness proofs span the entire development from the high-level abstra…