SoftwareApplication
name: Artifact to the paper "A Fast and Verified Probabilistic Model Checking Pipeline for Minimal Reachability Probabilities"
description: Artifact to the paper "A Fast and Verified Probabilistic Model Checking Pipeline for Minimal Reachability Probabilities"
description: This artifact contains the proofs of correctness of the Interval Iteration (II) pipeline including min-reduction 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 Fast and Verified Probabilistic Model Checking Pipeline for Minimal Reachability Probabilities" submitted at LOPSTR 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/4e5289d1-9fbf-47da-9f4c-9752c0321980.git
author: https://orcid.org/0000-0003-2908-8838
keywords: Markov decision process
keywords: Correct-by-construction
keywords: Interactive Theorem Proving
keywords: Probabilistic Model Checking
programming language: C
programming language: C++
programming language: JSON
programming language: Markdown
programming language: Other
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