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

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
choose version: version 2 - 2023-10-31 (latest)
version 1 - 2023-08-21

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)