Jobs/M2 2016 ER Multi-core for Spot

From LRDE

Development of Parallel Algorithms for Spot
Reference id

M2 2016 ER Multi-core for Spot

Dates

5-6 months in 2016

Research field

Model Checking

Related project

Spot

Advisor

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.

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

https://www.lrde.epita.fr/~renault/publis/TACAS15.pdf

  • Improved Multi-Core Nested Depth-First:

http://eprints.eemcs.utwente.nl/21967/01/cndfs.pdf

  • Scalable Multi-core LTL Model-Checking:

http://anna.fi.muni.cz/papers/src/public/bd4df1ce0205b57753ace9e3d208b618.pdf

Place LRDE: How to get to us
Compensation

1000 € gross/month

Future work opportunities

The internship can easily be prolonged as a PhD thesis.

Contact

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