TY - DATA
T1 - Artifact for the paper "A Formally Verified IEEE 754 Floating-Point Implementation of Interval Iteration for MDPs"
PY - 2025/04/11
AU - Bram Kohlen
AU - Maximilian Schäffeler
AU - Mohammad Abdulaziz
AU - Arnd Hartmanns
AU - Peter Lammich
UR - 
DO - 10.4121/bf0fef24-4f0f-4de6-a58d-07b9ba601804.v1
KW - IEEE 754
KW - Floating-point
KW - Correct-by-construction
KW - LLVM
KW - Interval Iteration
KW - Interactive Theorem Proving
KW - Software Verification
KW - Probabilistic Model Checking
KW - Markov Decision Process
N2 - <p>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).</p><p><br></p><p>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!</p>
ER -