LIP6 CNRS Sorbonne Université Tremplin Carnot Interfaces
Direct Link LIP6 » News » PhD students

HAMEZ Alexandre

PhD graduated
Team : MoVe
Departure date : 02/01/2010
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 - 14h00 - Site Passy-Kennedy - salle 549
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

2006-2010 Publications

 Mentions légales
Site map |