Presentation of the 9th Edition of the Model Checking Contest

Elvio Amparore, Bernard Berthomieu, Gianfranco Ciardo, Silvano Dal Zilio, Francesco Gallà, Lom Messan Hillah, Francis Hulin-Hubard, Peter Gjøl Jensen, Loïg Jezequel, Fabrice Kordon*, Didier Le Botlan, Torsten Liebke, Jeroen Meijer, Andrew Miner, Emmanuel Paviot-Adet, Jiří Srba, Yann Thierry-Mieg, Tom van Dijk, Karsten Wolf

*Corresponding author for this work

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

7 Citations (Scopus)
7 Downloads (Pure)

Abstract

The Model Checking Contest (MCC) is an annual competition of software tools for model checking. Tools must process an increasing benchmark gathered from the whole community and may participate in various examinations: state space generation, computation of global properties, computation of some upper bounds in the model, evaluation of reachability formulas, evaluation of CTL formulas, and evaluation of LTL formulas. For each examination and each model instance, participating tools are provided with upÂto 3600Âs and 16 gigabyte of memory. Then, tool answers are analyzed and confronted to the results produced by other competing tools to detect diverging answers (which are quite rare at this stage of the competition, and lead to penalties). For each examination, golden, silver, and bronze medals are attributed to the three best tools. CPU usage and memory consumption are reported, which is also valuable information for tool developers.

Original languageEnglish
Title of host publicationTools and Algorithms for the Construction and Analysis of Systems - 25 Years of TACAS
Subtitle of host publicationTOOLympics, Held as Part of ETAPS 2019, Proceedings
EditorsFabrice Kordon, Marieke Huisman, Bernhard Steffen, Dirk Beyer
PublisherSpringer Verlag
Pages50-68
Number of pages19
ISBN (Print)9783030175016
DOIs
Publication statusPublished - 4 Apr 2019
Event25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems conference series, TACAS 2019 - Charles University, Prague, Czech Republic
Duration: 6 Apr 201911 Apr 2019
Conference number: 25

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume11429 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems conference series, TACAS 2019
Abbreviated titleTACAS 2019
CountryCzech Republic
CityPrague
Period6/04/1911/04/19
Otherheld as part of the 22nd European Joint Conferences on Theory and Practice of Software, ETAPS 2019

Keywords

  • Competition
  • CTL formulas
  • LTL formulas
  • Model checking
  • Reachability formulas
  • State space

Fingerprint

Dive into the research topics of 'Presentation of the 9th Edition of the Model Checking Contest'. Together they form a unique fingerprint.

Cite this