Introduction

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.

I. Rules specific to Model Submission and their Publication

M-1.The Organizers of the Call for Models of the 2014 edition of the Model Checking Contest are: Hubert Garavel, Lom Hillah, and Fabrice Kordon.

M-2. The detailed instructions for proposing a model are given in the Call for Models and the model submission toolkit.

M-3. Any model submitted should be in the public domain. Any model that is proprietary, copyrighted, and/or confidential should not be submitted. Persons who submit a model hereby allow the organizers to freely use this model and publish it in the web if this model is selected.

M-4. If a submitted model is improper (e.g., invalid PNML file, missing or incomplete model description form, etc.), the organizers may contact the person(s) who submitted the model and ask for corrections. If corrections are not done or are unsatisfactory, the organizers can reject the model.

M-5. Among all submitted models, the Organizers will select approximately a dozen, according to criteria such as: originality, complexity, diversity with respect to other models, industrial relevance, etc.

M-6. The list of models selected for the 2014 edition of the Model Checking Contest will be kept confidential by the Organizers until all tools have been submitted, so that selected models are not known in advance by tool developers.

M-7. When the tool contest will start, selected models will be published on the contest web sites and the names of the authors of selected models will be mentioned on this same web site. The Organizers of the Call for Models will neither submit tools themselves, and will ensure fair competition between all tool developers competing in the Call for Tools.

II. Rules specific to Tool Submission and their Publication

T-1.The Organizers of the Call for Tools of the 2014 edition of the Model Checking Contest are: Francis Hulin-Hubard, Fabrice Kordon, and Alban Linard.

T-2. Developers of a tool (or a tool extension) can participate with their own work. Tools may also be submitted by others if they present the latest version available on the web.

T-3. All MCC models are provided in PNML, which is the input format for Petri nets. in principle, each submitted tool should be able to read these PNML files; if a tool is not capable of reading PNML, it may read alternative files provided by the submitter(s) in another format than PNML. This only stands for «known» models that are known when the call for tool is issued ; for «surprise» models, the use of PNML is mandatory

T-4. It is allowed to participate for certain models only and/or certain examinations only (e.g., state space generation, some types of formulas). See the Submission Manual for details.

T-5. Submitted tool must honestly perform the computations required by the MCC examinations. Using precomputed results is not allowed and, if detected, will disqualify the tool submission.

T-6. Each examination must be computed independently, i.e. without using previous results of an earlier computation. However, when a file contains several formulas, on can reuse the results of certain formulas to compute other formulas.

T-7. Participants authorize the publication of the MCC results.

Miscellaneous Provisions

P-1. In case of technical problems or litigious situations, participants should first discuss with the Organizers of the Call for Models, or Call for Tools, respectively.

P-2. Any issue that cannot be solved by discussion with the Organizers (call for models, call for tools) should be brought before Didier Buchs, who is one of the two General Chairs.

P-3. Withdrawal of a participating tool by the organizers at any moment is possible in case of not respecting the present rules.

P-4. A participating tool can resign at any moment, it will be completely removed from the record of the contest.

P-5. The Model Checking Contest is governed by French laws. Only the justice courts of Paris (France) are legally competent for settling disputes related to this contest.