Artifact to the paper "A Fast and Verified Probabilistic Model Checking Pipeline for Minimal Reachability Probabilities"

DOI:10.4121/37ae9db3-6a3d-4191-88c8-b843c12223b7.v1
The DOI displayed above is for this specific version of this dataset, which is currently the latest. Newer versions may be published in the future. For a link that will always point to the latest version, please use
DOI: 10.4121/37ae9db3-6a3d-4191-88c8-b843c12223b7

Datacite citation style

Kohlen, Bram (2025): Artifact to the paper "A Fast and Verified Probabilistic Model Checking Pipeline for Minimal Reachability Probabilities". Version 1. 4TU.ResearchData. software. https://doi.org/10.4121/37ae9db3-6a3d-4191-88c8-b843c12223b7.v1
Other citation styles (APA, Harvard, MLA, Vancouver, Chicago, IEEE) available at Datacite

Software

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.

History

  • 2025-06-02 first online, published, posted

Publisher

4TU.ResearchData

Format

.thy

Funding

  • NWO Open Competition OCENW.KLEIN.311: Verified Probabilistic Verification

Organizations

University of Twente, Faculty of Electrical Engineering, Mathematics and Computer Science (EEMCS), Formal Methods and Tools (FMT)

To access the source code, use the following command:

git clone https://data.4tu.nl/v3/datasets/4e5289d1-9fbf-47da-9f4c-9752c0321980.git

Or download the latest commit as a ZIP.