Master 2015 2016
Stages de la spécialité SAR
Development of Parallel Algorithms for Spot

Site : Development of Parallel Algorithms for Spot
Lieu : LRDE-EPITA 14 - 16 rue Voltaire 94276 Le Kremlin-Bicêtre Cedex
Encadrant : Etienne Renault, < renault at lrde . epita . fr >
Dates :Entre février et août 2016 (6 mois)
Rémunération :1000 Euros brut/mois
Mots-clés : Master SAR, autre qu’ATIAM


* General Representation of the field :

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 of the two previous automata and finally check wether the product automaton has an empty language. This last operation is called an emptiness check and deals with automata of millions of states and transitions. Recently many parallel emptiness checks have been proposed, each of them having strengths an weakness. Nonetheless it is still unknown if one of them outperform the others. Indeed, since all these algorithms are implemented in different tools, a fair comparison is impossible.

*Prerequisites :

- have some experience in multithreading and C++ programming
- like to write clean and optimized code
- Facilities with theoretical matters (especially Automata)

* Objectives : The goal of this internship is :
- 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 concurrent (possibly lock-free) data structures and algorithms.

* Future work opportunities : The internship can easily be prolonged as a PhD thesis.


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

Improved Multi-Core Nested Depth-First :

Scalable Multi-core LTL Model-Checking :