Difference between revisions of "Jobs/M2 2016 ER Multi-core for Spot"


Line 3: Line 3:
|Title=Development of Parallel Algorithms for Spot
|Title=Development of Parallel Algorithms for Spot
|Dates=5-6 months in 2016
|Dates=5-6 months in 2016
|Research field=Automata Theory
|Research field=Model Checking
|Related project=Spot
|Related project=Spot
|Advisor=Etienne Renault
|Advisor=Etienne Renault
Line 43: Line 43:
|Type=Master Internship
|Type=Master Internship

Revision as of 17:57, 30 November 2016

Development of Parallel Algorithms for Spot
Reference id

M2 2016 ER Multi-core for Spot


5-6 months in 2016

Research field

Model Checking

Related project



Etienne Renault

General presentation of the field

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 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.

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

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.
Benefit for the candidate
  • Parallel Explicit Model Checking for Generalized Büchi Automata:


  • Improved Multi-Core Nested Depth-First:


  • Scalable Multi-core LTL Model-Checking:


Place LRDE: How to get to us

1000 € gross/month

Future work opportunities

The internship can easily be prolonged as a PhD thesis.


< renault at lrde . epita . fr > < renault at lrde . epita . fr >