This artifact contains the proofs of correctness of an algorithm for Interval Iteration (II) 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 different data structures and a refinement to LLVM that is done using 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 by our modified version of mcsta to reproduce the experiments in our paper. To streamline the process, we have provided small scripts that perform basic tasks automatically (e.g. copying, moving, removing files and running mcsta).
This artifact is designed to run on a 64-bit Linux distribution (Docker available) with at least 32GB of RAM. Note that support of the AVX512 instruction set is a must to reproduce the benchmarks!
" authors: - family-names: Kohlen given-names: Bram orcid: "https://orcid.org/0000-0003-2908-8838" - family-names: Schäffeler given-names: Maximilian orcid: "https://orcid.org/0000-0002-2612-2335" - family-names: Abdulaziz given-names: Mohammad orcid: "https://orcid.org/0000-0002-8244-518X" - family-names: Hartmanns given-names: Arnd orcid: "https://orcid.org/0000-0003-3268-8674" - family-names: Lammich given-names: Peter orcid: "https://orcid.org/0000-0003-3576-0504" title: "Artifact for the paper "A Formally Verified IEEE 754 Floating-Point Implementation of Interval Iteration for MDPs"" keywords: version: 1 identifiers: - type: doi value: 10.4121/bf0fef24-4f0f-4de6-a58d-07b9ba601804.v1 license: BSD-3-Clause date-released: 2025-04-11