The doi 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/3f2a4539-e69b-4d16-b665-530c1abddfbc

Kohlen, Bram; Hartmanns, Arnd; Peter Lammich (2024): Artifact for the paper "Efficient Formally Verified Maximal End Component Decomposition for MDPs". Version 1. 4TU.ResearchData. software. https://doi.org/10.4121/3f2a4539-e69b-4d16-b665-530c1abddfbc.v1

Software

• Computation Theory and Mathematics
• Information and Computing Sciences

Correct-by-construction, Interactive Theorem Proving, Maximal End Components, Probabilistic Model Checking, Software Verification, Strongly Connected Components

BSD-3-Clause

RefWorks, BibTeX, Reference Manager, Endnote, DataCite, NLM, DC, CFF

by Bram Kohlen , Arnd Hartmanns , Peter Lammich

This artifact contains the proofs of correctness of an algorithm for maximal end component (MEC) decomposition 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 "Efficient Formally Verified Maximal End Component Decomposition for MDPs" accepted at FM 2024. The proof is divided into a correctness proof for the abstract algorithm, an 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 MEC 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 (or Virtual Machine) with at least 16GB, although we recommend 32 GB or more to run the benchmarks. It installations of clang, Isabelle/HOL with the AFP and python3. If you use the Virtualbox virtual machine, these will be preinstalled. This virtual machine is based on the TACAS23-AEC, username and password are tacas23.

The artifact contains a link to a git repository to run the artifact directly on your machine. If you would like to run the artifact in a virtual machine, download the mec-artifact-vm.ova file.

• 2024-06-21 first online, published, posted

4TU.ResearchData

.thy

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

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