Quantitative Verification Benchmark Set

 |  Materials  |  Reproducibility  |  Openness

The Quantitative Verification Benchmark Set is a collection of probabilistic models – Markov models, fault trees, stochastic Petri nets and others – to serve as a benchmark set for the benefit of algorithm and tool developers as well as the foundation of QComp.

Available Materials

The benchmark set comprises benchmark models, properties for verification, and tool results.


The benchmark set's models are


Every model is accompanied by a set of properties: queries for quantities of interest to be computed by analysis tools. The benchmark set collects models with queries for unbounded and bounded reachability probabilities, for unbounded and bounded variants of various forms of expected accumulated rewards, and for steady-state values.


Alongside its various models, the repository also provides tool results: property values and performance data obtained by applying different tools to the models across different hardware configurations.


Throughout, all data necessary for reproducibility is available, for example the command lines used to convert the models from their original modelling language into JANI or the precise hardware and runtime configuration that a set of results was obtained in.


The benchmark set is hosted on GitHub and accepts contributions.