Nicolas Amat, Elvio Amparore, Bernard Berthomieu, Pierre Bouvier, Silvano Dal Zilio, Francis Hulin-Hubard, Peter Gjøl Jensen, Loïg Jezequel, Fabrice Kordon, Shuo Li, Emmanuel Paviot-Adet, Laure Petrucci, Jiří Srba, Yann Thierry-Mieg, Karsten Wolf
In TOOLympics Challenge 2023 — Updates, Results, Successes of the Formal-Methods Competitions, nov 2024.
Abstract#
This paper takes you behind the scenes of the Model Checking Contest (MCC), an annual competition focusing on the behavioral analysis of asynchronous systems using state-space exploration and model checking techniques.
The MCC is part of a thriving group of scientific events dedicated to provide a fair evaluation of formal analysis tools, with the goal to push forward the state of the art and provide insights into the evolution of the involved technologies and approaches. We give details on the organization of the competition and on the ways we manage models and formulas. We also take a look at the evolution of the results over the 2018—2023 period, using the wide variety of data we collect each year, and report on the impact the MCC had on the competing tools.
Citation#
@InProceedings{DalzilioS:TOOLympics2023,
author = {Amat, Nicolas and Amparore, Elvio and Berthomieu, Bernard and Bouvier, Pierre and {Dal Zilio}, Silvano and Hulin-Hubard, Francis and Jensen, Peter Gjøl and Jezequel, Loïg and Kordon, Fabrice and Li, Shuo and Paviot-Adet, Emmanuel and Petrucci, Laure and Srba, Jiří and Thierry-Mieg, Yann and Wolf, Karsten},
title = {{Behind the Scene of the Model Checking Contest, Analysis of Results from 2018 to 2023}},
booktitle = {TOOLympics Challenge 2023 -- Updates, Results, Successes of the Formal-Methods Competitions},
series = {Lecture Notes in Computer Science},
volume = {14550},
publisher = {Springer-Verlag},
doi = {10.1007/978-3-031-67695-6_3},
month = nov,
year = 2024
}