Rules for Publication and Participation

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

2. (2)Computation must be effectively performed, precomputed results cannot be accepted.
   

3. (3)Life cycle of the virtual machine (if one is used) is limited to all instance of a particular model.
   

4. (4)State space is computed with the command (-generate), deadlocks are computed with the command (-deadlocks) and properties are checked with the command (-check). Results of commands -generate cannot be reused for command - deadlocks. Results of commands -generate and - deadlocks cannot be used for command -check.
   

5. (5)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.
   

6. (6)Command computation caches must be emptied before using (-generate) command, (-deadlock) command or (-check) command.
   

Rules for Computing Results

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

8. (8)Participants authorize result publication during workshop, on the web site and on the resulting publication. Additional comments from the authors on the results are encouraged and expected.
   

9. (9)Participation can be done only on a part of the tests (state space generation, deadlock, formulas) or only on a part of the models.
   

10. (10)Participants are providing sources or binaries for the benchmark computers. Benchmark computer characteristics are communicated by the organizers as precisely as possible.
    

11. (11)Result obtained by the benchmark computers are communicated as early as possible for detection and correction of possible problems.
    

Rules for Litigious Situations

12. (12)Only basic explanation of the used techniques are expected, for more detail use bibliographical references.
    

13. (13)In case of technical problems, participants and organizers communicate to solve the problems.
    

14. (14)Litigious situation are transmitted to the organizer that tries to solve the problems, no other entities can solve the complaints.
    

15. (15)Withdrawal of a participant by the organizer at any moment is possible in case of not respecting the present rules.
    

16. (16)A participant can resign at any moment, it will be completely removed from the record of the contest.
    

Model Checking Contest, Rules