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

Carlos E. Budde, Arnd Hartmanns, Michaela Klauck, Jan Kretínský, David Parker, Tim Quatmann, Andrea Turrini, Zhen Zhang

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

5 Citations (Scopus)
8 Downloads (Pure)

Abstract

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.

Original languageEnglish
Title of host publicationLeveraging Applications of Formal Methods, Verification and Validation
Subtitle of host publicationTools and Trends - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Proceedings
EditorsTiziana Margaria, Bernhard Steffen
Place of PublicationCham
PublisherSpringer
Pages216-241
Number of pages26
ISBN (Electronic)978-3-030-83723-5
ISBN (Print)978-3-030-83722-8
DOIs
Publication statusPublished - 5 Aug 2021
Event9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020 - Virtual Event
Duration: 20 Oct 202030 Oct 2020
Conference number: 9

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume12479
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020
Abbreviated titleISoLA 2020
CityVirtual Event
Period20/10/2030/10/20

Fingerprint

Dive into the research topics of 'On Correctness, Precision, and Performance in Quantitative Verification - QComp 2020 Competition Report'. Together they form a unique fingerprint.

Cite this