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


Description

The Spot library (https://spot.lrde.epita.fr/) 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.

Bibliographie

- On-The-Fly Parallel Decomposition of Strongly Connected Components https://pdfs.semanticscholar.org/26...

- Parallel Explicit Model Checking for Generalized Büchi Automata : https://www.lrde.epita.fr/ renault/...

- Improved Multi-Core Nested Depth-First : http://eprints.eemcs.utwente.nl/219...

- Scalable Multi-core LTL Model-Checking : http://anna.fi.muni.cz/papers/src/p...

- Distributed Algorithms for SCC Decomposition https://www.google.fr/url?sa=t&...