Model Checking Contest @ Petri Nets 2015
Bruxelles, Belgium, June 23, 2015
Home Page
Last Updated
August 19, 2015
August 19, 2015: full results are now available
June 14, 2015: About 4 years, 2 months and 18 days of CPU produced 24GByte of raw data
May 29, 2015: publication of the «surprise» models
May 26, 2015: the, list of qualified tools is known
April 13, 2015: final formulas provided, see instructions there
March 13, 2015: preliminary formula set for tests is provided
February 13, 2015: call for tools is out
December 31, 2014: the NUPN-toolspecific specification is available
December 9, 2014: a deadline extension is provided for model submission (7 models submitted at this stage)
December 8, 2014: update of model forms for past years (integration of data collected during the MCC'2014)
November 3, 2014: call for models is out

Results for the MCC@Petri Net 2015

If you want to cite the 2015 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 A. Hamez and E. Lopez-Bobeda and L. Jezequel and J. Meijer and E. Paviot-Adet
   and C. Rodriguez and C. Rohr and J. Srba and Y. Thierry-Mieg and K. Wolf},
   Howpublished = {{}},
   Lastchecked = {2015},
   Title = {{Complete Results for the 2015 Edition of the Model Checking Contest}},
   Urldate = {2015},
   Year = {2015}}

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

Examinations for Model Checkers

Several examinations are proposed:

Important dates

The Model Checking Contest will have several steps:

Results From Previous Editions

Scientific Papers Mentioning the Model Checking Contest

  1. Nested-Unit Petri Nets: A Structural Means to Increase Efficiency and Scalability of Verification on Elementary Nets (2015)
  2. Building a Symbolic Model Checker from Formal Language Description (2015)
  3. Saturation-Based Incremental LTL Model Checking with Inductive Proofs (2015)
  4. New Search Strategies for the Petri Net CEGAR Approach (2015)
  5. Bounded Model Checking High Level Petri Nets in PIPE+Verifier (2014)
  6. PeCAn: Compositional Verification of Petri Nets Made Easy (2014)
  7. Formal Modeling and Analysis Techniques for High Level Petri Nets (2014)
  8. Teaching formal methods: Experience at UPMC and UP13 with CosyVerif (2014)
  9. BenchKit, a Tool for Massive Concurrent Benchmarking (2014)
  10. Petri Nets Research at BTU in Cottbus, Germany (2014)
  11. Read, Write and Copy Dependencies for Symbolic Model Checking (2014)
  12. Compilation de réseaux de Petri : modèles haut niveau et symétries de processus (2014)
  13. Formal verification problems in a big data world: towards a mighty synergy (2014)
  14. Advanced Saturation-based Model Checking (2014)
  15. Compilation de réseaux de Petri (2013)
  16. Verifiable Design of a Satellite-based Train Control System with Petri Nets (2014)
  17. Unifying the syntax and semantics of modular extensions of Petri nets (2013)
  18. Modeling and Analyzing Wireless Sensor Networks with VeriSensor : An Integrated Workflow (2013)
  19. Building Petri nets tools around Neco compiler (2013)
  20. LTL Model Checking with Neco (2013)
  21. MaRDiGraS : Simplified Building of Reachability Graphs on Large Clusters (2013)
  22. CosyVerif: An Open Source Extensible Verification Environment (2013)
  23. A Modular Approach for Reusing Formalisms in Verification Tools of Concurrent Systems (2013)
  24. Unifying the syntax and semantics of modular extensions of Petri nets (2013)
  25. Half a century after Carl Adam Petri’s Ph.D. thesis: A perspective on the field (2013)
  26. Verification based on unfoldings of Petri nets with read arcs (2013)
  27. High-level Petri net model checking : the symbolic way (2012)
  28. Stubborn Sets for Simple Linear Time Properties (2012)
  29. High-Level Petri Net Model Checking with AlPiNA (2011)
  30. Crocodile : A Symbolic/Symbolic Tool for the Analysis of Symmetric Nets with Bag (2011)