Jobs/M2 2017 MC Spot demo


Interactive Spot demonstration
Reference id

M2 2017 MC Spot demo


5-6 months in 2018

Research field

Model checking

Related project



Alexandre Duret-Lutz, Étienne Renault, Maximilien Colange

General presentation of the field

The Spot library ( contains many algorithms for translating LTL formulas into omega-automata, and to simplify these formulas and automata. It also provides support to build an LTL model checker, through algorithms testing whether the language of such an automaton is empty or not.

The model-checking process takes a model of a system and a LTL formula to check, and outputs either "correct" if the property holds, or a run of the system on which the property does not hold (a counterexample).


This internship targets students who:

  • have some experience in Web development and/or C++ and/or Python (conjunction is favored over disjunction)
  • would like to get familiar with the amazing world of model-checking
  • would like to popularize model-checking and formal methods

We wish to build an interactive, web-based demonstration prototype for Spot, to illustrate the interest of model checking. The targeted use-case is the verification of a controller for lifts.

The prototype should provide several functionalities, among which:

  • a graphical representation of the system and its evolution,
  • a way to specify a controller and to check temporal properties by calling Spot.
  • the capability to replay (graphically) a counter-example given by Spot.
  • the ability to describe the characteristics of the lifts system (number of lifts, ranges etc.)

Such a prototype is intended to be used in the communication of the LRDE, for example during the Journées Portes Ouvertes.

Another module would consist in a game on LTL. The game picks a LTL formula (at random, or among a list of pre-selected patterns), and displays a corresponding omega-automaton to the player. The goal is to find the original LTL formula. When the player makes a wrong guess, the game could help her with traces recognized by the secret formula but not by the player's formula.

Benefit for the candidate

Place LRDE: How to get to us

1000 € gross / month

Future work opportunities

<at> colange <at>