LIP6 CNRS Sorbonne Université Tremplin Carnot Interfaces
Direct Link LIP6 » أحـداث السـاعـة » مسجلون في الدكتوراه

HAMEZ Alexandre

وحـدة : MoVe
تاريـخ المـغادرة : 01/02/2010
رئاسـة البـحث : Fabrice KORDON
تأطـير مـشـترك : 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.
مناقـشـة مـذكـرة : 08/12/2009 - 14h00 - Site Passy-Kennedy - salle 549
أعـضاء لجنة المناقـشة :
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

 Mentions légales
| خـريـطـة المـوقـع