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/aff9f553-0e9e-4ec2-90e0-20c5b6152862

Hartmanns, Arnd; Kohlen, Bram; Peter Lammich (2023): Artifact for the Paper "Fast Verified SCCs for Probabilistic Model Checking". Version 2. 4TU.ResearchData. software. https://doi.org/10.4121/aff9f553-0e9e-4ec2-90e0-20c5b6152862.v2

Version 1 - 2023-08-21

Usage statistics

Categories

• Computer Software
• Computation Theory and Mathematics
• Information and Computing Sciences

Keywords

correct-by-construction Gabow IRF Isabelle Refinement Framework Isabelle/HOL Linear programming Markov chain Markov decision process Model Checking Modest toolset Probabilistic model checking Probabilistic timed automata Program verification SCC Strongly connected components Topological value iteration

Time coverage

26-07-2023

Licence

MIT

Export as...

RefWorks BibTeX Reference Manager Endnote DataCite NLM DC CFF

by Arnd Hartmanns , Bram Kohlen , Peter Lammich

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.

History

• 2023-08-21 first online

• 2023-10-31 published, posted

Publisher

4TU.ResearchData

Format

.thy files

Associated peer-reviewed publication

Fast Verified SCCs for Probabilistic Model Checking

References

• https://www21.in.tum.de/~lammich/gabow_scc_modest/

Funding

• NWO Open Competition OCENW.KLEIN.311: Verified Probabilistic Verification
• European Union's Horizon 2020 research and innovation program (grant code STG–677576) European Research Council
• NWO VENI 639.021.754

Organizations

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