Results for the MCC@Petri Net 2016

Thanks to K. Wolf, the results for 2015 and 2016 have been organized in a mysql database that you may gather here (73.3 MB). Since some bugs in some models have been detected after the 2015 and 2016 editions of the model checking, some results may not be reproducable from the updated version of the PNML files that you can get from the model page.

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

@misc{mcc:2016, Author = {F. Kordon and H. Garavel and L. M. Hillah and F. Hulin-Hubard and G. Chiardo and A. Hamez and L. Jezequel and A. Miner and J. Meijer and E. Paviot-Adet and D. Racordon and C. Rodriguez and C. Rohr and J. Srba and Y. Thierry-Mieg and G. Tr{\d i}nh and K. Wolf}, Howpublished = {{http://mcc.lip6.fr/2016/results.php}}, Lastchecked = {2016}, Urldate = {2016}, Month = {June}, Title = {{Complete Results for the 2016 Edition of the Model Checking Contest}}, Year = {2016}}

This should look like to this (useful for those who prefer word-like word processors ;-):

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 five editions in 2011, 2012, 2013, 2014, and 2015 this is the sixth one that will take place at PETRI NETS 2016 in Torun.

Results of the Previous Editions

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

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

Nov. 03, 2015: publication of the Call for Models
Nov. 16, 2015: publication of the Call for Tools
Dec. 10, 2015: 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)
Dec. 10, 2015: publication of the Tool Submission Kit, which will be made available from http://mcc.lip6.fr/archives/ToolSubmissionKit.tar.gz
Jan. 15, 2016: publication of the updated 2016 contest rules at http://mcc.lip6.fr/rules.php
Apr. 15, 2016: deadline for tool submission
Apr. 30, 2016: early feedback to tool submitters, following the preliminary qualification runs, which are performed using a few small instances of the "known" models
June 1st, 2016: more feedback to tool submitters, following the competition runs
June 21, 2016: official announcement of MCC'2016 results during the Petri Net conference (Torun, Poland)

Results for the MCC@Petri Net 2016

Objectives

Results of the Previous Editions

Important dates

Scientific Papers Mentioning the Model Checking Contest