HomeRulesCfPCall for ModelsOrganizersMCC 2011
Model Checking Contest @ PETRI NETS 2012
Hamburg, Germany, June 25-29 2012
Model Checking Contest - Rules

Rules for Publication and Participation

R01: Only the developers of a tool (or a tool extension) can participate with their own work.

R02: Computation must be effectively performed, precomputed results cannot be accepted unless for parts specified in the examination.

R03:Life cycle of the virtual machine is limited to an instance of a particular model.

R04: Each command -check must be performed independently, i.e. without using previous results of an earlier (-check) command. When a file contains several formulas, then computation for the evaluation of a formula can be reused for another one.

Rules for Computing Results

R05: Tools must be freely available for the PC members of the contest (at least as an academic license).

R06: Participants authorize result publication, on the web site and on the resulting publication. Additional comments from the authors on the results are encouraged and expected.

R07: Participation can be done only on a part of the tests (state space generation, some types of formulas) or only on a part of the models. Then, the tool must provide an explicit answer (see the Submission Manual).

R08: For colored models, tools may either choose the colored version or the equivalent P/T version. This choice must be the same for all the instances of a given model.

R09: Participants are providing sources or binaries for the benchmark in a disk-image to be used in a Virtual Machine. Benchmark characteristics and instructions are communicated by the organizers as precisely as possible (see the Submission Manual).

R10: Result obtained by the benchmark computers are communicated as early as possible for detection and correction of possible problems.

R11: Tool can exploit structural properties of a model only when they are provided.

R12: Organizers make all their possible to select the "push-button model" to evaluate the push-button mode at the very last minute, when all tool are already submitted. This, in order to be sure that no participant might be advantaged.

Rules for Litigious Situations

R13: Only basic explanations of the used techniques are expected, for more detail use bibliographical references.

R14: In case of technical problems, participants and organizers communicate to solve the problems.

R15: Litigious situation are transmitted to the organizer who tries to solve the problems, no other entities can solve the complaints.

R16: Withdrawal of a participant by the organizers at any moment is possible in case of not respecting the present rules.

R17: A participant can resign at any moment, it will be completely removed from the record of the contest.