The quantitative verification benchmark set

Arnd Hartmanns, Michaela Klauck, David Parker, Tim Quatmann, Enno Ruijters

Research output: Chapter in Book/Report/Conference proceedingConference contribution

10 Citations (Scopus)
215 Downloads (Pure)

Abstract

We present an extensive collection of quantitative models to facilitate the development, comparison, and benchmarking of new verification algorithms and tools. All models have a formal semantics in terms of extensions of Markov chains, are provided in the Jani format, and are documented by a comprehensive set of metadata. The collection is highly diverse: it includes established probabilistic verification and planning benchmarks, industrial case studies, models of biological systems, dynamic fault trees, and Petri net examples, all originally specified in a variety of modelling languages. It archives detailed tool performance data for each model, enabling immediate comparisons between tools and among tool versions over time. The collection is easy to access via a client-side web application at qcomp.org with powerful search and visualisation features. It can be extended via a Git-based submission process, and is openly accessible according to the terms of the CC-BY license.
Original languageEnglish
Title of host publicationTools and Algorithms for the Construction and Analysis of Systems. TACAS 2019
EditorsD. Beyer, M. Huisman, F. Kordon, B. Steffen
PublisherSpringer
Pages344–350
Number of pages7
Volume1
ISBN (Electronic)978-3-030-17502-3
ISBN (Print)978-3-030-17501-6
DOIs
Publication statusE-pub ahead of print - 4 Apr 2019
Event25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'19), - Prague, Czech Republic
Duration: 6 Apr 201911 Apr 2019

Publication series

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

Conference

Conference25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'19),
Country/TerritoryCzech Republic
CityPrague
Period6/04/1911/04/19

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint

Dive into the research topics of 'The quantitative verification benchmark set'. Together they form a unique fingerprint.

Cite this