TY - GEN
T1 - On Correctness, Precision, and Performance in Quantitative Verification
T2 - 9th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2020
AU - Budde, Carlos E.
AU - Hartmanns, Arnd
AU - Klauck, Michaela
AU - Křetínský, Jan
AU - Parker, David
AU - Quatmann, Tim
AU - Turrini, Andrea
AU - Zhang, Zhen
N1 - Publisher Copyright:
© 2021, Springer Nature Switzerland AG.
PY - 2021
Y1 - 2021
N2 - Quantitative verification tools compute probabilities, expected rewards, or steady-state values for formal models of stochastic and timed systems. Exact results often cannot be obtained efficiently, so most tools use floating-point arithmetic in iterative algorithms that approximate the quantity of interest. Correctness is thus defined by the desired precision and determines performance. In this paper, we report on the experimental evaluation of these trade-offs performed in QComp 2020: the second friendly competition of tools for the analysis of quantitative formal models. We survey the precision guarantees—ranging from exact rational results to statistical confidence statements—offered by the nine participating tools. They gave rise to a performance evaluation using five tracks with varying correctness criteria, of which we present the results.
AB - Quantitative verification tools compute probabilities, expected rewards, or steady-state values for formal models of stochastic and timed systems. Exact results often cannot be obtained efficiently, so most tools use floating-point arithmetic in iterative algorithms that approximate the quantity of interest. Correctness is thus defined by the desired precision and determines performance. In this paper, we report on the experimental evaluation of these trade-offs performed in QComp 2020: the second friendly competition of tools for the analysis of quantitative formal models. We survey the precision guarantees—ranging from exact rational results to statistical confidence statements—offered by the nine participating tools. They gave rise to a performance evaluation using five tracks with varying correctness criteria, of which we present the results.
UR - http://www.scopus.com/inward/record.url?scp=85115151033&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-83723-5_15
DO - 10.1007/978-3-030-83723-5_15
M3 - Conference contribution
AN - SCOPUS:85115151033
SN - 9783030837228
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 216
EP - 241
BT - Leveraging Applications of Formal Methods, Verification and Validation
A2 - Margaria, Tiziana
A2 - Steffen, Bernhard
PB - Springer Science and Business Media Deutschland GmbH
Y2 - 20 October 2020 through 30 October 2020
ER -