Jobs/M2 2019 MC Spot Distribued

From LRDE

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 >