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 | |
Advisor | |
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 |
|
Objectives |
The goal of this internship is:
|
Benefit for the candidate | |
References |
https://www.lrde.epita.fr/~renault/publis/TACAS15.pdf
http://eprints.eemcs.utwente.nl/21967/01/cndfs.pdf
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 > |