Presentation of the 9th Edition of the Model Checking Contest
Elvio Amparore
(1)
,
Bernard Berthomieu
(2)
,
Gianfranco Ciardo
(3)
,
Silvano Dal Zilio
(2)
,
Francesco Gallà
,
Lom Messan Hillah
(4, 5)
,
Francis Hulin-Hubard
(6)
,
Peter Gjøl Jensen
,
Loïg Jezequel
(7, 8)
,
Fabrice Kordon
(5)
,
Didier Le Botlan
(2)
,
Torsten Liebke
(9)
,
Jeroen Meijer
(10, 11)
,
Andrew Miner
,
Emmanuel Paviot-Adet
(10, 11, 5)
,
Jiří Srba
(12)
,
Yann Thierry-Mieg
(5)
,
Tom van Dijk
(11, 10)
,
Karsten Wolf
1
UNITO -
Università degli studi di Torino = University of Turin
2 LAAS-VERTICS - Équipe Verification de Systèmes Temporisés Critiques
3 Duke University [Durham]
4 UPN - Université Paris Nanterre
5 MoVe - Modélisation et Vérification
6 LIP6
7 UN - Université de Nantes
8 LS2N - Laboratoire des Sciences du Numérique de Nantes
9 Institut für Informatik [Rostock]
10 University of Twente
11 UPD5 - Université Paris Descartes - Paris 5
12 Department of Computer Science [Aalborg]
2 LAAS-VERTICS - Équipe Verification de Systèmes Temporisés Critiques
3 Duke University [Durham]
4 UPN - Université Paris Nanterre
5 MoVe - Modélisation et Vérification
6 LIP6
7 UN - Université de Nantes
8 LS2N - Laboratoire des Sciences du Numérique de Nantes
9 Institut für Informatik [Rostock]
10 University of Twente
11 UPD5 - Université Paris Descartes - Paris 5
12 Department of Computer Science [Aalborg]
Elvio Amparore
- Function : Author
- PersonId : 944022
Bernard Berthomieu
- Function : Author
- PersonId : 3451
- IdHAL : bernard-berthomieu
- ORCID : 0000-0001-9895-0052
- IdRef : 15975044X
Silvano Dal Zilio
- Function : Author
- PersonId : 3545
- IdHAL : dalzilio
- ORCID : 0000-0002-6002-2696
- IdRef : 123897912
Francesco Gallà
- Function : Author
Lom Messan Hillah
- Function : Author
- PersonId : 847
- IdHAL : lom-messan-hillah
- ORCID : 0000-0002-4558-720X
- IdRef : 13991238X
Peter Gjøl Jensen
- Function : Author
Loïg Jezequel
- Function : Author
- PersonId : 17349
- IdHAL : loig-jezequel
- ORCID : 0000-0001-5113-9668
- IdRef : 169378837
Fabrice Kordon
- Function : Author
- PersonId : 9774
- IdHAL : fabrice-kordon
- ORCID : 0000-0002-5626-828X
- IdRef : 074605283
Didier Le Botlan
- Function : Author
- PersonId : 13978
- IdHAL : didier-le-botlan
- IdRef : 168060949
Andrew Miner
- Function : Author
Emmanuel Paviot-Adet
- Function : Author
- PersonId : 971651
Yann Thierry-Mieg
- Function : Author
- PersonId : 174399
- IdHAL : yann-thierry-mieg
- ORCID : 0000-0001-7775-1978
- IdRef : 08901846X
Karsten Wolf
- Function : Author
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.