Jobs/M2 2019 MC Spot Distribued

	Distributed Model Checking
Reference id	M2 2019 MC Spot Distribued
Dates	5-6 months in 2019
Research field	Model checking, Distributed Algorithms and data structures
Related project	Spot
Advisor	Étienne Renault
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).
Prerequisites	This internship targets students who: have some experience in multithreaded/distributed and C++ programming like to write clean and optimized code facilities with theoretical matters (especially Automata)
Objectives	We wish to build a distributed model-checker so that we can outcome the limitation (time and memory) of multithreaded algorithms. The internship aims: 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 distributed data structures and algorithms.
Benefit for the candidate
References	One-Sided Communications for more Efficient Parallel State Space Exploration over RDMA Clusters https://www-lipn.univ-paris13.fr/~coti/papiers/CEP18.pdf On-The-Fly Parallel Decomposition of Strongly Connected Components https://pdfs.semanticscholar.org/2644/fb1d8009fccee7900524bf6ddd0f3fd8431c.pdf 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 Distributed Algorithms for SCC Decomposition https://core.ac.uk/download/pdf/81957312.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 >