On Correctness, Precision, and Performance in Quantitative
Verification - QComp 2020 Competition Report

D 2020

On Correctness, Precision, and Performance in Quantitative Verification - QComp 2020 Competition Report

BUDDE, Carlos E; Arnd HARTMANNS; Michaela KLAUCK; Jan KŘETÍNSKÝ; David PARKER et al.

Základní údaje

Originální název

On Correctness, Precision, and Performance in Quantitative Verification - QComp 2020 Competition Report

Autoři

BUDDE, Carlos E; Arnd HARTMANNS; Michaela KLAUCK; Jan KŘETÍNSKÝ; David PARKER; Tim QUATMANN; Andrea TURRINI a Zheng Hao ZHANG

Vydání

Leveraging Applications of Formal Methods, Verification and Validation: Tools and Trends - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20-30, 2020, Proceedings, Part IV, od s. 216-241, 26 s. 2020

Nakladatel

Springer

Další údaje

Typ výsledku

Stať ve sborníku

Označené pro přenos do RIV

Organizační jednotka

Fakulta informatiky

ISBN

9783030837228

ISSN

DOI

https://doi.org/10.1007/978-3-030-83723-5_15

Změněno: 17. 3. 2025 14:43, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

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.

Citovat

BUDDE, Carlos E; Arnd HARTMANNS; Michaela KLAUCK; Jan KŘETÍNSKÝ; David PARKER; Tim QUATMANN; Andrea TURRINI a Zheng Hao ZHANG. On Correctness, Precision, and Performance in Quantitative Verification - QComp 2020 Competition Report. In Leveraging Applications of Formal Methods, Verification and Validation: Tools and Trends - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20-30, 2020, Proceedings, Part IV. Springer, 2020, s. 216-241. ISBN 9783030837228. Dostupné z: https://doi.org/10.1007/978-3-030-83723-5_15.

@inproceedings{2484794,
   author = {Budde, Carlos E and Hartmanns, Arnd and Klauck, Michaela and Křetínský, Jan and Parker, David and Quatmann, Tim and Turrini, Andrea and Zhang, Zheng Hao},
   booktitle = {Leveraging Applications of Formal Methods, Verification and Validation: Tools and Trends - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20-30, 2020, Proceedings, Part IV},
   doi = {https://doi.org/10.1007/978-3-030-83723-5_15},
   isbn = {9783030837228},
   pages = {216-241},
   publisher = {Springer},
   title = {On Correctness, Precision, and Performance in Quantitative Verification - QComp 2020 Competition Report},
   year = {2020}
}

TY  - CONF
ID  - 2484794
AU  - Budde, Carlos E - Hartmanns, Arnd - Klauck, Michaela - Křetínský, Jan - Parker, David - Quatmann, Tim - Turrini, Andrea - Zhang, Zheng Hao
PY  - 2020
TI  - On Correctness, Precision, and Performance in Quantitative Verification - QComp 2020 Competition Report
PB  - Springer
SN  - 9783030837228
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.
ER  -

BUDDE, Carlos E; Arnd HARTMANNS; Michaela KLAUCK; Jan KŘETÍNSKÝ; David PARKER; Tim QUATMANN; Andrea TURRINI a Zheng Hao ZHANG. On Correctness, Precision, and Performance in Quantitative Verification - QComp 2020 Competition Report. In \textit{Leveraging Applications of Formal Methods, Verification and Validation: Tools and Trends - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20-30, 2020, Proceedings, Part IV}. Springer, 2020, s.~216-241. ISBN~9783030837228. Dostupné z: https://doi.org/10.1007/978-3-030-83723-5\_{}15.

Přehled o publikaci