qcomp.org is the home of the QVBS: the Quantitative Verification Benchmark Set, and of QComp: the Comparison of Tools for the Analysis of Quantitative Formal Models. The source code for this website is mostly CC-BY 4.0-licensed and available on GitHub.
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. 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 replicability 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.
The Comparison of Tools for the Analysis of Quantitative Formal Models (QComp) is the friendly competition among verification and analysis tools for quantitative formal models. Drawing its benchmarks from the Quantitative Verification Benchmark Set, it compares the performance, versatility, and usability of the participating tools.