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. https://doi.org/10.4121/aff9f553-0e9e-4ec2-90e0-20c5b6152862.v1
Other citation styles (APA, Harvard, MLA, Vancouver, Chicago, IEEE) available at Datacite
Software

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, published, posted
publisher
4TU.ResearchData
format
.thy files
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)

DATA

files (2)