Master 2017 2018
Stages de la spécialité SAR
Distributed Model Checking

Site : Distributed Model Checking
Lieu : LRDE-EPITA 14-16 rue Voltaire 94276 Le Kremlin-Bicêtre Cedex
Encadrant : Etienne Renault
Dates :5 - 6 mois en 2018
Rémunération :1000 € brut/mois
Mots-clés : Master SAR, autre qu’ATIAM

Cliquer ici pour vous authentifier


The Spot library ( written in C++11 offers several algorithms and data structures to build model checkers. Such a tool checks whether the model of a system meets a given specification. One way to perform this verification is to encode both the specification and the model as omega-automata, build the synchronous product.

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 multithreaded/distributed and C++ programming

- like to write clean and optimized code

- facilities with theoretical matters (especially Automata)

We wish to build a distributed model-checker so that we can outcome the limitation (time and memory) of multithreaded algorithms. The internship aims :

- to implement optimized scalable versions of state-of-the-art emptiness checks

- to evaluate relative performances of each of them

- to help in the development of the thread-safe part of the Spot library by adding distributed data structures and algorithms.


- On-The-Fly Parallel Decomposition of Strongly Connected Components

- Parallel Explicit Model Checking for Generalized Büchi Automata : renault/...

- Improved Multi-Core Nested Depth-First :

- Scalable Multi-core LTL Model-Checking :

- Distributed Algorithms for SCC Decomposition