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

doi:10.4121/aff9f553-0e9e-4ec2-90e0-20c5b6152862

Ctrl K

Software Projects Organisations Communities News

Ctrl K

.css-1e132ge{font-family:-apple-system,BlinkMacSystemFont,'Segoe UI',Roboto,'Helvetica Neue',Arial,sans-serif,'Apple Color Emoji','Segoe UI Emoji','Segoe UI Symbol';font-weight:400;font-size:0.875rem;line-height:1.43;background-color:transparent;display:-webkit-box;display:-webkit-flex;display:-ms-flexbox;display:flex;padding:6px 16px;color:rgb(96, 54, 20);background-color:rgb(253, 243, 234);width:100vw;-webkit-box-pack:center;-ms-flex-pack:center;-webkit-justify-content:center;justify-content:center;margin-top:1rem;z-index:9;}.css-1e132ge .MuiAlert-icon{color:#ed6c02;}.css-1pl9tfm{background-color:#fff;color:rgba(34,36,37,1);-webkit-transition:box-shadow 300ms cubic-bezier(0.4, 0, 0.2, 1) 0ms;transition:box-shadow 300ms cubic-bezier(0.4, 0, 0.2, 1) 0ms;border-radius:2px;box-shadow:var(--Paper-shadow);background-image:var(--Paper-overlay);overflow:auto;font-family:-apple-system,BlinkMacSystemFont,'Segoe UI',Roboto,'Helvetica Neue',Arial,sans-serif,'Apple Color Emoji','Segoe UI Emoji','Segoe UI Symbol';font-weight:400;font-size:0.875rem;line-height:1.43;background-color:transparent;display:-webkit-box;display:-webkit-flex;display:-ms-flexbox;display:flex;padding:6px 16px;color:rgb(96, 54, 20);background-color:rgb(253, 243, 234);width:100vw;-webkit-box-pack:center;-ms-flex-pack:center;-webkit-justify-content:center;justify-content:center;margin-top:1rem;z-index:9;}.css-1pl9tfm .MuiAlert-icon{color:#ed6c02;}

Limited functionality: Your browser does not support JavaScript.

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

mentions

contributors

Get started

Description

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.

Keywords

Correct-by-construction

Gabow

IRF

Isabelle/HOL

Isabelle Refinement Framework

Linear programming

Markov chain

Markov decision process

Model Checking

Modest toolset

Probabilistic Model Checking