SoftwareApplication
name: Artifact for the paper "Efficient Formally Verified Maximal End Component Decomposition for MDPs"
description: Artifact for the paper "Efficient Formally Verified Maximal End Component Decomposition for MDPs"
description: 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.
code repository: https://data.4tu.nl/v3/datasets/a80bcdc5-8fc3-419f-897c-bfaf18fdd21f.git
author: https://orcid.org/0000-0003-2908-8838
author: https://orcid.org/0000-0003-3268-8674
author: https://orcid.org/0000-0003-3576-0504
keywords: Software Verification
keywords: Correct-by-construction
keywords: Strongly Connected Components
keywords: Interactive Theorem Proving
keywords: Probabilistic Model Checking
keywords: Maximal End Components
programming language: C
programming language: C++
programming language: JSON
programming language: Markdown
programming language: Other
programming language: Python
programming language: Shell
programming language: TeX
programming language: XML
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-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