[Lrde Annonce] Soutenance de thèse de E. Renault

Bonjour, J'ai le plaisir de vous convier à ma soutenance de thèse qui aura lieu le Vendredi 5 Décembre 2014 à 14h en salle salle 211 - tour 55 - couloir 55/65 - 2ème étage. La soutenance sera suivie d’un pot. Sujet de la thèse : « Contribution aux tests de vacuité pour le model checking explicite » Membre du jury : Laure. Petrucci (Professeur à l’Université Paris 13): rapporteur Francois Vernadat (Professeur à l’INSA toulouse): rapporteur Jean-Michel. Couvreur (Professeur à l’Université d’Orléans) : examinateur Emmanuelle Encrenaz (Maitre de conférence à l’Université Paris 6): examinateur Jaco van de Pol (Professeur à l’Université de Twente): examinateur Alexandre Duret-Lutz (Maitre de conférence à l’EPITA): encadrant de thèse D. Poitrenaud (Maitre de conférence à l’Université Paris 6): encadrant de thèse Fabrice Kordon (Professeur à l’Université Paris 6): Directeur de thèse Plan d’accès : http://www.upmc.fr/fr/universite/campus_et_sites/a_paris_et_en_idf/jussieu.… Résumé : ———— L'approche automate pour le model checking de propriétés temporelles à temps linéaire est une technique classique de vérification formelle de systèmes concurrents. Un système, ainsi qu'une propriété qu'on souhaite y vérifier, sont modélisés sous forme d’omega-automates reconnaissant des mots infinis. Des manipulations de ces automates (produit synchronisé et test de vacuité) permettent d'établir si le système vérifie la propriété ou non. Dans cette thèse nous nous focalisons sur un type particulier d'omega-automates qui permettent une représentation concise des propriétés d'équité faible: les automates de Büchi généralisés basés sur les transitions (TGBA ou Transition-based Generalized Büchi Automata). Dans un premier temps, nous brossons un aperçu des algorithmes de vérification existant et nous en proposons de nouveaux traitant efficacement les automates généralisés forts. Dans un second temps, l'analyse des composantes fortement connexes de l'automate de la propriété nous a conduit à élaborer une décomposition de cet automate. Cette décomposition se focalise sur les automates multi-forces et permet une parallélisation naturelle des model-checkers. Enfin, nous avons proposé les premiers tests de vacuité parallèles pour les automates généralisés. De plus, tous ces tests sont lock-free à la différence de ceux de l’état de l’art. Toutes ces techniques ont ensuite été implémentées et évaluées sur un jeu de test conséquent. Abstract : ———— The automata-theoretic approach to linear time model-checking is a standard technique for formal verification of concurrent systems. The system and the property to check are modeled with omega-automata that recognizes infinite words. Operations overs these automata (synchronized product and emptiness checks) allows to determine whether the system satisfies the property or not. In this thesis we focus on a particular type of omega-automata that enable a concise representation of weak fairness properties: transitions-based generalized Büchi automata (TGBA). First we outline existing verification algorithms, and we propose new efficient algorithms for strong automata. In a second step, the analysis of the strongly connected components of the property automaton led us to develop a decomposition of this automata. This decomposition focuses on multi-strength property automata and allows a natural parallelization for already existing model-checkers. Finally, we proposed, for the first time, new parallel emptiness checks for generalized Büchi automata. Moreover, all these emptiness checks are lock-free, unlike those of the state-of-the-art. All these techniques have been implemented and then evaluated on a large benchmark.