HAMEZ Alexandre

doctorant à Sorbonne Université
Équipe : MoVe
https://www.linkedin.com/in/alexandrehamez/?ppe=1

Direction de recherche : Fabrice KORDON

Co-encadrement : THIERRY-MIEG Yann

Génération efficace de grands espaces d'états

Garantir la fiabilité des systèmes informatiques exige des moyens de vérification rigoureux. Le model checking est une technique de vérification dont l’intérêt majeur est l’automatisation, et donc la facilité d’utilisation pour les ingénieurs. La récente attribution du prix Turing aux créateurs de cette technique atteste de sa viabilité. Le model checking explore exhaustivement les modèles analysés. Cela amène un problème majeur : l’explosion combinatoire liée aux espaces d'états des grands systèmes. Depuis plus de vingt ans, de nombreuses solutions ont été proposées pour repousser cette limite de taille afin d’être capable de traiter des espaces d’états toujours plus grands dont les tailles peuvent atteindre très rapidement les 10^400 éléments. Les travaux présentés ici proposent deux types de solutions pour traiter plus efficacement de plus grands espaces d’états. La première s'appuie sur les ressources de calcul parallèle des machines multi-processeurs, omniprésentes aujourd’hui, et des grappes de calcul. La deuxième propose de traiter plus efficacement les diagrammes de décision en automatisant la technique dite de saturation, dont l’efficacité empiriquement montrée est très difficile à atteindre manuellement.

Soutenance : 08/12/2009

Membres du jury :

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

Date de départ : 01/02/2010

Publications 2006-2010