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.
ER -