SoftwareApplication
name: Artifact for the paper "A Formally Verified IEEE 754 Floating-Point Implementation of Interval Iteration for MDPs"
description: Artifact for the paper "A Formally Verified IEEE 754 Floating-Point Implementation of Interval Iteration for MDPs"
description: 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.
code repository: https://data.4tu.nl/v3/datasets/e5db01c4-34b5-4bd9-adc0-b9a32a1b9057.git
author: https://orcid.org/0000-0003-2908-8838
author: https://orcid.org/0000-0002-2612-2335
author: 0000-0002-8244-518X
author: https://orcid.org/0000-0003-3268-8674
author: https://orcid.org/0000-0003-3576-0504
keywords: Markov decision process
keywords: Software Verification
keywords: Correct-by-construction
keywords: Interval Iteration
keywords: Floating-point
keywords: LLVM
keywords: Interactive Theorem Proving
keywords: Probabilistic Model Checking
keywords: IEEE 754
programming language: C
programming language: C++
programming language: JSON
programming language: Markdown
programming language: Other
programming language: Python
programming language: Shell
programming language: TeX
license:
  creative work: creativeWork
    name: BSD-3-Clause

https://orcid.org/0000-0003-2908-8838
type: Person
given name: Bram
family name: Kohlen
name: Bram Kohlen

https://orcid.org/0000-0002-2612-2335
type: Person
given name: Maximilian
family name: Schäffeler
name: Maximilian Schäffeler

0000-0002-8244-518X
type: Person
given name: Mohammad
family name: Abdulaziz
name: Mohammad Abdulaziz

https://orcid.org/0000-0003-3268-8674
type: Person
given name: Arnd
family name: Hartmanns
name: Arnd Hartmanns

https://orcid.org/0000-0003-3576-0504
type: Person
given name: Peter
family name: Lammich
name: Peter Lammich