Difference between revisions of "Jobs/M2 2016 ER Multi-core for Spot"
From LRDE
(Created page with "{{Job |Reference id=M2 2016 ER Multi-core for Spot |Title=Development of Parallel Algorithms for Spot |Dates=5-6 months in 2016 |Research field=Automata Theory |Related proje...") |
|||
Line 19: | Line 19: | ||
them having strengths an weakness. Nonetheless it is still unknown if one |
them having strengths an weakness. Nonetheless it is still unknown if one |
||
of them outperform the others. Indeed, since all these algorithms are implemented |
of them outperform the others. Indeed, since all these algorithms are implemented |
||
− | in different tools, a fair comparison is impossible. |
+ | in different tools, a fair comparison is impossible. |
− | |||
|Prerequisites=* have some experience in multithreading and C++ programming |
|Prerequisites=* have some experience in multithreading and C++ programming |
||
* like to write clean and optimized code |
* like to write clean and optimized code |
||
* facilities with theoretical matters (especially Automata) |
* facilities with theoretical matters (especially Automata) |
||
− | |||
|Objectives=The goal of this internship is: |
|Objectives=The goal of this internship is: |
||
* to implement optimized scalable versions of state-of-the-art emptiness checks |
* to implement optimized scalable versions of state-of-the-art emptiness checks |
||
* to evaluate relative performances of each of them |
* 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. |
+ | * to help in the development of the thread-safe part of the Spot library by adding concurrent (possibly lock-free) data structures and algorithms. |
|References=* Parallel Explicit Model Checking for Generalized Büchi Automata: |
|References=* Parallel Explicit Model Checking for Generalized Büchi Automata: |
||
Line 40: | Line 38: | ||
http://anna.fi.muni.cz/papers/src/public/bd4df1ce0205b57753ace9e3d208b618.pdf |
http://anna.fi.muni.cz/papers/src/public/bd4df1ce0205b57753ace9e3d208b618.pdf |
||
⚫ | |||
− | |||
⚫ | |||
|Compensation=1000 € gross/month |
|Compensation=1000 € gross/month |
||
|Future work opportunities=The internship can easily be prolonged as a PhD thesis. |
|Future work opportunities=The internship can easily be prolonged as a PhD thesis. |
Revision as of 16:22, 20 November 2015
Development of Parallel Algorithms for Spot | |
---|---|
Reference id |
M2 2016 ER Multi-core for Spot |
Dates |
5-6 months in 2016 |
Research field |
Automata Theory |
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 > |