This artifact contains the proofs of correctness of the Interval Iteration (II) algorithm for MDPs as well as a modified version of mcsta from the Modest Toolset with models to reproduce the benchmarks. The high-level proofs are described in the paper "A Formally Verified IEEE 754 Floating-Point Implementation of Interval Iteration for MDPs" accepted at CAV 2025. The proof is divided into a correctness proof for the abstract algorithm, a proof of correctness for the underlying data structures, and a refinement to LLVM performed within the Isabelle Refinement Framework. Running the proofs yields an LLVM implementation of the II algorithm.
Once compiled into a library, it can directly be used in our modified version of mcsta to reproduce the experiments from our paper. To streamline the process, we provide scripts that perform the tasks automatically (e.g. copying, moving, removing files and running the benchmarks).
This artifact is designed to run on a 64-bit Linux distribution (we include a Docker image) with internet access and at least 32GB of RAM and support for the AVX512 instruction set. If you do not use Docker, it requires installations of Isabelle 2025 including the AFP, clang and optionally, python.
ER -