View source for Affiche-these-AB

{{DISPLAYTITLE:PhD Defense Ala Eddine Ben Salem}}

<div class="center" style="width: auto; margin-left: auto; margin-right: auto;">[[File:lip6.png|80px]]  &nbsp;  [[File:UPMC.png|126px]]  &nbsp;  [[File:Logo EPITA Ingenieur BLEU 3.JPG|110px]]  &nbsp;  [[File:Lrde.png|110px]] &nbsp; 
</div>


<div class="center" style="width: auto; margin-left: auto; margin-right: auto;"><big>'''SOUTENANCE de THESE'''</big>
</div>

<div class="center" style="width: auto; margin-left: auto; margin-right: auto;"><big>'''ALA EDDINE BEN SALEM'''</big>
</div>

<div class="center" style="width: auto; margin-left: auto; margin-right: auto;"><big>''' JEUDI 25 SEPTEMBRE 2014 '''</big>
</div>

<div class="center" style="width: auto; margin-left: auto; margin-right: auto;"><big>''' A 14H00 '''</big>
</div>

<div class="center" style="width: auto; margin-left: auto; margin-right: auto;"><big>''' Salle 203, bâtiment 41 '''</big>
</div>

<div class="center" style="width: auto; margin-left: auto; margin-right: auto;"><big>''' , LIP6, UPMC, Paris-Jussieu '''</big>
</div>

<div class="center" style="width: auto; margin-left: auto; margin-right: auto;">Plan d’accès : http://www.upmc.fr/fr/universite/campus_et_sites/a_paris_et_en_idf/jussieu.html
</div>


<div class="center" style="width: auto; margin-left: auto; margin-right: auto;"><big>''' IMPROVING THE MODEL CHECKING OF STUTTER-INVARIANT LTL PROPERTIES'''</big>
</div>


'''Abstract:'''

Les systèmes logiciels sont devenus omniprésents se substituant à l’homme pour des tâches délicates, souvent critiques, mettant en jeu des coûts importants voire des vies humaines. Les conséquences des défaillances imposent la recherche de méthodes rigoureuses pour la validation des systèmes. L’approche par automates du model-checking est la plus classique des approches de vérification automatique. Elle prend en entrée un modèle du système et une propriété, et permet de savoir si cette dernière est vérifiée. Pour cela un model-checker traduit la négation de la propriété en un automate et vérifie si le produit du système et de cet automate est vide. Hélas, bien qu’automatique, cette approche souffre d'une explosion combinatoire du nombre d’états du produit obtenu.
Afin de combattre ce problème, en particulier lors de la vérification des propriétés insensibles au bégaiement, nous proposons la première évaluation d’automates testeur (TA) sur des modèles réalistes, une amélioration de l’algorithme de vérification pour ces automates et une méthode permettant de transformer un TA en un automate (STA) permettant une vérification en une seule passe.
Nous proposons aussi une nouvelle classe d’automates: les TGTA. Ces automates permettent une vérification en une seule passe sans ajouter d’états artificiels. Cette classe combine les avantages des TA et des TGBA (automates de Büchi). Les TGTA permettent d’améliorer les approches explicite et symbolique de model-checking. Notamment, en combinant les TGTA avec la technique de saturation, les performances de l'approche symbolique  sont améliorées d’un ordre de grandeur par rapport aux TGBA.
Utilisés dans l’approche hybride les TGTA se révèlent complémentaires aux TGBA.


'''Composition du Jury :'''

* MATEESCU Radu Mateescu (INRIA), Rapporteur
* SCHWOON Stefan (ENS Cachan), Rapporteur
* BÉRARD Béatrice  (UPMC, Paris 6), Examinateur
* BUCHS Didier (Université de Genève), Examinateur
* KORDON Fabrice (UPMC, Paris 6), Directeur de thèse
* DURET-LUTZ Alexandre (EPITA, LRDE), Encadrant