Team : MoVe
Departure date : 12/07/2016

From Symbolic Verification to Domain Specific Languages

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.

Defence : 12/07/2016

Jury members :

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

Associate Professor

4 PhD graduated 2009 - 2013

Mentions légales
Site map