PhD Defense Etienne Renault

From LRDE


Lip6.png   UPMC.png   Epita.png   Lrde.png  


SOUTENANCE de THESE
ETIENNE RENAULT
VENDREDI 5 DECEMBRE 2014
A 14H00
Salle 211 - tour 55 - couloir 55/65
LIP6, UPMC, Paris-Jussieu


CONTRIBUTIONS TO EMPTINESS CHECKS FOR EXPLICIT MODEL CHECKING


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.



Thesis committee:

  • PETRUCCI Laure (Professor, University of Paris 13): Reporter
  • VERNADAT François (Professor, INSA Toulouse): Reporter
  • COUVREUR Jean-Michel (Professor, University of Orléans): Examiner
  • ENCRENAZ Emmanuelle (Assistant-Professor, UPMC, Paris 6): Examiner
  • VAN DE POL Jaco (Professor, University of Twente): Examiner
  • DURET-LUTZ Alexandre (Assistant-Professor, EPITA, LRDE): Co-advisor
  • POITRENAUD D. (Assistant-Professor, UPMC, Paris 6): Co-advisor
  • KORDON Fabrice (Professor, UPMC, Paris 6): Principal advisor