Behind the Scene of the Model Checking Contest, Analysis of Results from 2018 to 2023

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.