TY - DATA T1 - Artifact for the Paper "Fast Verified SCCs for Probabilistic Model Checking" PY - 2023/10/31 AU - Arnd Hartmanns AU - Bram Kohlen AU - Peter Lammich UR - DO - 10.4121/aff9f553-0e9e-4ec2-90e0-20c5b6152862.v2 KW - Model Checking KW - Strongly connected components KW - SCC KW - Modest toolset KW - Isabelle/HOL KW - Isabelle Refinement Framework KW - IRF KW - Gabow KW - Program verification KW - correct-by-construction N2 -

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.

ER -