Quantitative Verification Benchmark Results

↪  |  License: CC-BY 4.0  |  Contributing  |   JANI Converters

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.

Select data
Tools

Versions

Models
()

Parameters

Properties
Configure display
Show   per   and   as a 
Results
Results
Notes
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.