LIP6 CNRS Sorbonne Université Tremplin Carnot Interfaces
Direct Link LIP6 » Actualité » Doctorants


Habilitation à Diriger des Recherches
Équipe : MoVe

De la vérification symbolique aux langages spécifiques au domaine (traduction Google)

This talk will present our experience in building data structures, algorithms, languages and tools to enable symbolic model-checking of specifications expressed in a variety of formalisms. The data structures use symbolic representations of large sets of states and of transition relations to face the challenge of state space explosion, inherent to model-checking. The algorithms exploit such symbolic representations to verify complex behavioral properties of a system, expressed using temporal logic.
We leverage model-driven engineering and model transformations to propose a simple yet expressive intermediate language to express the semantics of concurrent systems.
The tools freely available at offer both a user friendly front-end and an efficient back-end solver. They support analysis of diverse formalisms designed for modeling of concurrent and real-time systems.
Soutenance : 07/12/2016 - 14h00 - RC entre tour 22 et 23
Membres du jury :
Professeur Claude JARD - Univ. Nantes [rapporteur]
Professeur Richard PAIGE - Univ. York, UK [rapporteur]
Professeur Jaco VAN DE POL - Univ. Twente, NL [rapporteur]
Professeur Ahmed BOUAJJANI - Univ. Paris Diderot
Professeur Jean-Michel COUVREUR - Univ. Orléans
Professeur Serge HADDAD - ENS Cachan
Professeur Fabrice KORDON - Univ. Paris 6
Professeur François VERNADAT - INSA Toulouse

4 Docteurs 2009 - 2013

 Mentions légales
Carte du site |