Artifact for the Paper "Fast Verified SCCs for Probabilistic Model Checking"

doi: 10.4121/aff9f553-0e9e-4ec2-90e0-20c5b6152862.v1
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/aff9f553-0e9e-4ec2-90e0-20c5b6152862
Datacite citation style:
Hartmanns, Arnd; Kohlen, Bram; Peter Lammich (2023): Artifact for the Paper "Fast Verified SCCs for Probabilistic Model Checking". Version 1. 4TU.ResearchData. software.
Other citation styles (APA, Harvard, MLA, Vancouver, Chicago, IEEE) available at Datacite

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.

  • 2023-08-21 first online, published, posted
.thy files
  • 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
University of Twente, Faculty of Electrical Engineering, Mathematics and Computer Science (EEMCS), Formal Methods and Tools (FMT)


files (2)