Quantitative Verification Benchmark Results
The models and results in this benchmark set on qcomp.org are provided under the terms of the
CC-BY 4.0 license.
Please cite the publication linked as "first presented in" for each model.
To contribute a new model, update an existing model, or add new results for an existing model, please consider our
information for contributors.
For general questions or comments concerning the benchmark set, contact
If you have questions concerning a specific model, please contact the submitter listed for that model.
Per-property runtimes include overhead: the difference between the total runtime and the sum of the individual per-property runtimes of a result.
A result's overhead is evenly distributed over all properties included in the result.
Overhead may include e.g. the time for tool startup and state space exploration.
The CPU-scaled runtime is obtained by multiplying the actual runtime in seconds by one-thousandth of the Passmark
"single-thread rating" for the CPU of the system that the result was obtained on.
It is a unitless number meant to improve the fairness of comparing runtimes obtained on different systems and has no absolute meaning.