SoftwareApplication
name: Artifact for the Paper "Fast Verified SCCs for Probabilistic Model Checking"
description: Artifact for the Paper "Fast Verified SCCs for Probabilistic Model Checking"
description: The artifact that backs up the data in our ATVA 2023 Paper titled "Fast Verified SCCs for Probabilistic Model Checking". This artifact contains the proof files for Isabelle/HOL. Running the proofs yields a LLVM implementation of Gabow's algorithm that can be compiled to a dynamic library. This artifact also contains a version of the Modest toolset that can use this library to replace the built-in SCC algorithm. Lastly, the artifact contains scripts that reproduce the results in the paper. The additional reference contains a link to browsable version of the artifact that allows proofs to be inspected without downloading anything.
author: https://orcid.org/0000-0003-3268-8674
author: https://orcid.org/0000-0003-2908-8838
author: https://orcid.org/0000-0003-3576-0504
keywords: Markov decision process
keywords: Gabow
keywords: Program verification
keywords: Model Checking
keywords: Isabelle/HOL
keywords: Topological value iteration
keywords: Correct-by-construction
keywords: SCC
keywords: Markov chain
keywords: Linear programming
keywords: IRF
keywords: Probabilistic timed automata
keywords: Modest toolset
keywords: Strongly Connected Components
keywords: Probabilistic Model Checking
keywords: Isabelle Refinement Framework
license:
  creative work: creativeWork
    name: MIT
reference publication: 978-3-031-45329-8 9

https://orcid.org/0000-0003-3268-8674
type: Person
given name: Arnd
family name: Hartmanns
name: Arnd Hartmanns

https://orcid.org/0000-0003-2908-8838
type: Person
given name: Bram
family name: Kohlen
name: Bram Kohlen

https://orcid.org/0000-0003-3576-0504
type: Person
given name: Peter
family name: Lammich
name: Peter Lammich

978-3-031-45329-8 9
type: ScholarlyArticle
name: Fast Verified SCCs for Probabilistic Model Checking
pagination: 181-202
url: https://doi.org/10.1007%2F978-3-031-45329-8_9