Pre-registration

IMPORTANT: if, as a tool developer, you are interested in submitting your tool for the MCC'2020, please register using the form below. You will then be added to the mailing-list and be alerted of any information concerning the Model Checking Contest. You might also be contacted for checking certain choices concerning the examination.

List of the Examinations Model Checkers can participate in

Several examinations are proposed:

• State space generation: tools will have to generate the state space and provide data on its size,
• Evaluation of models upper bound: tools will have to process the maximum number of tokens in some parts of the models,
• Evaluation of global properties: tools will have to process true and false model independent properties,
• Evaluation of reachability properties: tools will have to process true and false reachability properties, stating for each one if it is verified or not,
• Evaluation of Linear Temporal Logic properties (LTL): tools will have to process true and false properties, stating for each one if it is verified or not,
• Evaluation of Computation Tree Logic properties (CTL): tools will have to process true and false properties, stating for each one if it is verified or not.