Jobs/M2 2019 MC Spot Distribued
|Distributed Model Checking|
M2 2019 MC Spot Distribued
5-6 months in 2019
Model checking, Distributed Algorithms and data structures
|General presentation of the field||
The Spot library (https://spot.lrde.epita.fr/) written in C++14 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
The model-checking process takes a model of a system and a LTL formula to check, and outputs either "correct" if the property holds, or a run of the system on which the property does not hold (a counterexample).
This internship targets students who:
We wish to build a distributed model-checker so that we can outcome the limitation (time and memory) of multithreaded algorithms. The internship aims:
|Benefit for the candidate|
|Place||LRDE: How to get to us|
1000 € gross/month
|Future work opportunities||
The internship can easily be prolonged as a PhD thesis.