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.
After nine editions in 2011, 2012, 2013, 2014, 2015, 2016, 2017, 2018, and 2019 this is the tenth one that will take place in Paris, aside the Petri Net conference.
Results of the Previous Editions
Below is a quick access to the results of the past editions of the Model Checking Contest:
- 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
- December 15, 2019: publication of the Call for Models
- January 15, 2020: publication of the Call for Tools
- January 25, 2020: publication of the updated 2020 contest rules at http://mcc.lip6.fr/rules.php
- January 31, 2020: publication of the Tool Submission Kit, which will be made available from http://mcc.lip6.fr/archives/ToolSubmissionKit.tar.gz
- March 1, 2020: deadline for model submission
- March 1, 2020: deadline for tool pre-registration If you plan to submit a tool to the contest, please fill in the pre-registration form (you may retire if you finally decide not to do so)
- April. 1, 2020: individual notification of model acceptance/rejection
- April 15, 2020: deadline for tool submission
- May 1, 2020: early feedback to tool submitters, following the preliminary qualification runs, which are performed using a few small instances of the "known" models
- June 1, 2020: on-line publication of the selected MCC'2020 models
- June 23, 2020: official announcement of MCC'2020 results during the Petri Net conference (Paris, France).