LIP6 CNRS Sorbonne Université Tremplin Carnot Interfaces
Direct Link LIP6 » Tin tức » Nghiên cứu sinh
https://www.lrde.epita.fr/~renault/

RENAULT Etienne

Tiến sĩ()
Nhóm nghiên cứu : MoVe
Ngày đi : 31-12-2014
https://www.lrde.epita.fr/~renault/
Ban lãnh đạo nghiên cứu : Fabrice KORDON
Đồng hướng dẫn : DURET-LUTZ Alexandre, POITRENAUD Denis

Contribution aux tests de vacuité pour le model checking explicite

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.
Bảo vệ luận án : 05-12-2014 - 14h - Site Jussieu 55-65/211
Hội đồng giám khảo :
Laure. Petrucci (Professeur à l'Université Paris 13) [rapporteur]
Francois Vernadat (Professeur à l'INSA toulouse) [rapporteur]
Jean-Michel. Couvreur (Professeur à l'Université d’Orléans)
Emmanuelle Encrenaz (Maitre de conférence à l'Université Paris 6)
Jaco van de Pol (Professeur à l'Université de Twente)
Alexandre Duret-Lutz (Maitre de conférence à l'EPITA)
D. Poitrenaud (Maitre de conférence à l'Université Paris 5)
Fabrice Kordon (Professeur à l'Université Paris 6)

1 Nghiên cứu sinh (Ban lãnh đạo nghiên cứu / Đồng hướng dẫn)

Bài báo khoa học 2010-2019

 Mentions légales
Sơ đồ site |