Introduction

As suggested during the MCC'2023 discussions, we are organizing a workshop dedicated to the Model Checking Contest @ ETAPS'2023. This event will take place on Sunday April 23 in Paris at Institut Henri Poincaré.

Objectives

The objective of this workshop is to bring together developers and organizers in order to discuss several issues aside the model checking contest that could be useful for the involved communities.

Several topics can be considered (non exclusive list):

• Discussion among tool developers about the new techniques they operated for the contest.
• Identification of a core semantics for Petri nets with time that could enable the creation of a new examination track dealing with timed properties. Please refer to the MCC rules for a definition of what an examination is.
• Some tutorial like the integration of a tool in the framework of the competition or how to operate the execution environment itself.
• Etc.

Please find enclosed the program to take place at Institut Henri Poincarré on Sunday April 23, 2023.

How to participate (closed)

An abstract sketching (2-4 LNCS pages) the main points you want to discuss must be provided in order to let the organizers to establish a program. From the discussions, a paper could be issued by participants in a special issue or a volume dedicated to this event.

If you want to make a presentation, please contact the organizers. Please send your email before March 20, 2023.

You just have to register for a one day workshop at ETAPS'2023 (or more if you also attend other ETAPS events). It will be possible for a small number of participants to be there remotely if you really cannot make it to Paris (as for all ETAPS and associated events, this requires a registration).

Committee

• Pierre Bouvier, University of Grenoble Alpes
• Fabrice Kordon, Sorbonne Université
• Hubert Garavel, Inria
• Francis Hulin-Hubard, CNRS
• Loïg Jézéquel, Université de Nantes
• Emmanuel paviot-Adet, Université Paris Cité