HAMEZ Alexandre

PhD student at Sorbonne University
Team : MoVe
https://www.linkedin.com/in/alexandrehamez/?ppe=1

Supervision : Fabrice KORDON

Co-supervision : THIERRY-MIEG Yann

Efficient generation of large state spaces

Ensuring the reliability of computer systems requires the usage of rigorous verification. Model checking is a technique of verification whose major advantage is automation, and therefore the ease of use for engineers. The recent attribution of the Turing Award to the creators of this technique proves its viability.
The model checking exhaustively explores the models analyzed. This causes a major problem : combinatorial explosion due to the state spaces of large systems. For over twenty years, many solutions have been proposed to push the limit of size to be able to handle spaces states increasingly large sizes which can reach very quickly the 10^400 elements.
The work presented here offer two types of solutions to address more effectively larger spaces of states. The first relies on resources parallel computing machines with multiple CPUs, ubiquitous today, and cluster computing. The second proposed deal more effectively with decision diagrams by automating technique called saturation, whose effectiveness empirically shown is very difficult to achieve manually.

Defence : 12/08/2009

Jury members :

Didier Buchs, Professeur à l'Université de Genève [Rapporteur]
Patrice Moreaux Professeur à l'Université de Savoie [Rapporteur]
Béatrice Bérard Professeur à l'Université Paris 6
Alexandre Duret-Lutz Maître de Conférences à l'EPITA
François Vernadat Professeur à l'INSA Toulouse
Yann Thierry-Mieg Maître de Conférences à l'Université Paris 6
Fabrice Kordon Professeur à l'Université Paris 6

Departure date : 02/01/2010

2006-2010 Publications