Results for the MCC 2024

Important Note : we lately discovered a problem with the colored instances of BlocksWorld leading to a problem with results for 2024. We thus updated data from the contest by not considering these instances for 2024 (we will deal with corrections to be done for 2025)

As it is this year again a remote event, the MCC results will be out in two steps:

If you want to cite the 2024 MCC report, please proceed as follows (bibtex entry):

@misc{mcc:2024,
	Author = {F. Kordon and P. Bouvier and H. Garavel and F. Hulin-Hubard and
		L. Jezequel and E. Paviot-Adet Q. Nivon and and N. Amat. and B. Berthomieu  and
		S. {Dal Zilio} and {P. G.} Jensen and D. Morard and B. Smith and J. Srba and 
		Y. Thierry-Mieg and K. Wolf},
	Howpublished = {{https://mcc.lip6.fr/2024/results.php}},
	Lastchecked = 2024,
	Month = {June},
	Title = {{Complete Results for the 2024 Edition of the Model Checking Contest}},
	Urldate = {2024},
	Year = {2024}}

Objectives

The Model Checking Contest is a yearly scientific event dedicated to the assessment of formal verification tools for concurrent systems.

The Model Checking Contest has two different parts: the Call for Models, which gathers Petri net models proposed by the scientific community, and the Call for Tools, which benchmarks verification tools developed within the scientific community.

The objective of the Model Checking Contest is to compare the efficiency of techniques according to characteristics of models. To do so, the Model Checking Contest compares tools on several classes of models with scaling capabilities (e.g. values that set up the «size» of its associated state space). Through the feedback on tools efficiency according to the selected benchmarks, we aim at identifying the techniques that can tackle a given type of problem (e.g. state space generation, deadlock detection, reachability analysis, causal analysis).

The Model Checking Contest is composed of two calls: a call for models and a call for tools.

There was already thirteen editions in 2011, 2012, 2013, 2014, 2015, 2016, 2017, 2018, 2019, 2020, 2021, 2022, and 2023. This is the fourteenth edition that will take place during the Petri Net 2024 (Geneva, Switzerland).

Results of the Previous Editions

Below is a quick access to the results of the past editions of the Model Checking Contest:

MCC'2023 @ Paris: slides - HTML report
MCC'2022 @ Bergen: slides - HTML report
MCC'2021 @ Paris: video - HTML report
MCC'2020 @ Paris: video - HTML report
MCC'2019 @ Prague: slides - HTML report
MCC'2018 @ Bratislava: slides - HTML report
MCC'2017 @ Zaragoza: slides - HTML report
MCC'2016 @ Torún: slides - HTML report
MCC'2015 @ Brussels: slides - HTML report
MCC'2014 @ Tunis: slides - HTML report
MCC'2013 @ Milano: slides - HTML report - PDF report (CoRR)
MCC'2012 @ Hamburg: slides - PDF report (CoRR)
MCC'2011 @ Newcastle: slides - report (ToPnoC link)

Important dates

January 15, 2024: publication of the Call for Models
January 22, 2024: publication of the Call for Tools.
February 23, 2024: publication of the updated contest rules for 2023 at http://mcc.lip6.fr/2024/pdf/rules.pdf
February 24, 2024: publication of the Tool Submission Kit, which is available from https://mcc.lip6.fr/2024/archives/SubmissionKit.tar.gz
April 15, 2024: deadline for tool pre-registration If you plan to submit a tool to the contest, please fill in the pre-registration form available from http://mcc.lip6.fr/registration.php
May 1st, 2024: deadline for tool submission
May 15, 2024: deadline for model submission (for the MCC'2024)
May 15, 2024: early feedback to tool submitters, following the preliminary qualification runs, which are performed using a few small instances of the "known" models.
June 1st, 2024: individual notification of model acceptance/rejection
June 10, 2024: more feedback to tool submitters, following the competition runs
June 15, 2024: on-line publication of the selected MCC'2024 models
June 25, 2024: announcement of MCC'2024 results during the Petri Net Conference conference (Geneva, Switzerland)