Jobs/M2 2019 MC Spot Distribued


Distributed Model Checking
Reference id

M2 2019 MC Spot Distribued


5-6 months in 2019

Research field

Model checking, Distributed Algorithms and data structures

Related project



Étienne Renault

General presentation of the field

The Spot library ( 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:

  • have some experience in multithreaded/distributed and C++ programming
  • like to write clean and optimized code
  • facilities with theoretical matters (especially Automata)

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
  • One-Sided Communications for more Efficient Parallel State Space Exploration over RDMA Clusters

  • On-The-Fly Parallel Decomposition of Strongly Connected Components

  • Parallel Explicit Model Checking for Generalized Büchi Automata:

  • Improved Multi-Core Nested Depth-First:

  • Scalable Multi-core LTL Model-Checking:

  • Distributed Algorithms for SCC Decomposition

Place LRDE: How to get to us

1000 € gross/month

Future work opportunities

The internship can easily be prolonged as a PhD thesis.


< renault at lrde . epita . fr > < renault at lrde . epita . fr >