Authors

The authors are the main organizers, as well as the ones who submitted tools. The full list is provided below:

Fabrice Kordon, Univ. P. & M.Curie, France Alban Linard, Inria and École Normale Supérieure de Cachan, France Marco Beccuti, Univ. Torino, Italy Didier Buchs, Univ. Geneva, Switzerland Lukasz Fronc, Univ. Evry-Val-d'Essone, France Lom-Messan Hillah, Univ. Paris Ouest Nanterre, France Francis Hulin Hubard, CNRS and École Normale Supérieure de Cachan, France Fabrice Legond-Aubry, Univ. Paris Ouest Nanterre, France Niels Lohmann, Univ Rostock, Germany

Alexis Marechal, Univ. Geneva, Switzerland Emmanuel Paviot-Adet, Univ. René Descartes, France Franck Pommereau, Univ. Evry-Val-d'Essone, France César Rodríguez, École Normale Supérieure de Cachan, France Christian Rohr, Univ. Cottbus Germany Yann Thierry-Mieg, Univ. P. & M.Curie, France Haro Wimmel, Univ. Rostock, Germany Karsten Wolf, Univ. Rostock, Germany

Please do reference this web report as follows:

• F. Kordon, A. Linard, M. Becutti, D. Buchs, L. Fronc, F. Hulin-Hubard, F. Legond-Aubry, N. Lohmann, A. Marechal, E. Paviot-Adet, F. Pommereau, C. Rodrígues, C. Rohr, Y. Thierry-Mieg, H. Wimmel, and K. Wolf. Web report on the model checking contest @ petri net 2013, available at http://mcc.lip6.fr, June 2013.

or, in bibtex, as follows:

@misc{mcc2013web,
   Author = {F. Kordon and A. Linard and M. Becutti and D. Buchs and L. Fronc and F. Hulin-Hubard
   and F. Legond-Aubry and N. Lohmann and A. Marechal and E. Paviot-Adet and F. Pommereau and C. Rodr\'igues
   and C. Rohr and Y. Thierry-Mieg and H. Wimmel and K. Wolf},
   Month = {June},
   Title = {Web Report on the Model Checking Contest @ Petri Net 2013, available at http://mcc.lip6.fr},
   Year = {2013}}

Introduction

This page summarizes the results of this the Model Checking Contest @ Petri Nets 2013 (Milano, Italy). You can have access to the results, all the generated charts and to the scoring of the participating tools.

Model Contributors

The section below list the people who provided models to the various editions of the Model Checking Contest. Sometime, they are authors of these models, otherwise, they have summarized or retrieved an existing model from the literature... thus, they are "responsible" for these and, since they were of great help for establishing the base of our benchmark, we list them here below:

• J. Ezpeleta & F. Tricas García (Univ. Zaragoza, Spain): RessAllocation
• S. Evangelista (Univ. Paris 13, France): LamportFastMutEx, NeoElection, SimpleLoadBal
• H. Garavel (Inria, France): Vasy2003
• L. Hillah (Univ. Paris Ouest Nanterre): DrinkVendingMachine, FMS, Kanban, MAPK, Philosopher, SharedMemory
• F. Kordon (Univ. P. & M. Curie, France): GlobalRessAlloc, HouseConstruction, PermAdmissibility, QuasiCertifProtocol
• A. Linard (ENS de Cachan, France): CSRepetition, PhilosophersDyn
• N. Lohmann (Univ. Rostock, Germany): Echo, IBMB2S565S3960, PLanning, Ring, RwMutex
• A. Marechal (Univ. Geneva, Switzerland): TokenRing
• E. Paviot-Adet (Univ. René Descartes, France): DotAndBoxes, Peterson
• F. Pommereau (Univ. Evry Val d'Essone, France): Eratosthenes, Railroad
• C. Rodríguez (ENS de Cachan, France): Dekker

Data About the Model Checking Contest

Facts about the MCC’2013

Information about Participating tools

Techniques reported to be used by Tools for the MCC’2013

Computed Results

Results for the “known” models

Results for the “surprise” models

Computed Charts and Tables

Performance Charts

How Models Are Supported by Tools

Trophies

Summary of the winners per examination

Open Issues

Open issues