Model Checking Contest @ Petri Nets 2014
Tunis, Tunisia, June 24, 2014
Last Updated
Sept. 1, 2014
September 1st, 2014: results are now available
June 3, 2014: the 15 surprise models are published (full archive with formulas here ).
We are pleased to announce that 9 tools participate this year (with newwbies):
cunf, greatspn, helena, lola, marcie, pnmc, pnxdd, stratagem, tapaal
March 31, 2014: the call for tool participation has been updated (the benchmark).
You must either download the call for tool submission or patch your virtual machine if you already modified it (instructions provided).
March 3, 2014: the call for tool participation is out.
February 18, 2014: all model forms for «known» models have been updated with structural properties,
PNML files are also available for each model basis for testing purposes.
February 18, 2014: 15 «surprise» models have been selected for MCC 2014
(to be published when tools are submitted).

Results for the MCC@Petri Net 2014

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

  Author = {F. Kordon and H. Garavel and L-M. Hillah and F. Hulin-Hubard and A. Linard and
            M. Beccuti and S. Evangelista and A. Hamez and N. Lohmann and E. Lopez and
            E. Paviot-Adet and C. Rodriguez and C. Rohr and J. Srba},
  Howpublished = {{}},
  Lastchecked = {2014},
  Title = {{HTML results from the Model Checking Contest @ Petri Net (2014 edition)}},
  Urldate = {2014},
  year = {2014}}

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


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 identified in a «typical mode», for a given class 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 tool participation.

After three editions in 2011, 2012 and 2013, this is the fourth one that will take place at PETRI NETS 2014 in Tunis.

Examinations for Model Checkers

Several examinations are proposed:

Important dates

The Model Checking Contest will have several steps:

Results From Previous Editions

:wq :wq :q :q!