LIP6 CNRS Sorbonne Université Tremplin Carnot Interfaces
Direct Link LIP6 » أحـداث السـاعـة » مسجلون في الدكتوراه

DURET-LUTZ Alexandre

رخصة بإدارة البحوث()
وحـدة : MoVe

Contributions au LTL et ω-automata pour le Model Checking

We present multiple practical contributions to the automata-theoretic approach to LTL model checking. Most of these contributions are implemented in Spot (https://spot.lrde.epita.fr/), a library and a set of tools exporting reusable algorithms, with a growing user base.
In particular, we will present an overview of the techniques used in our LTL-to-Büchi translator, that is now one of the leading tools available for this task. We will also discuss how we built algorithms that support automata with arbitrary acceptance conditions, and how some of these algorithms became more elegant as a consequence.
Finally we will show how the set of tools that we have built can be used to improve existing algorithms by finding bugs or detecting nonoptimal results (e.g., by using a SAT-solver to find minimal deterministic omega-automata of arbitrary acceptance conditions).
مناقـشـة مـذكـرة : 10/02/2017 - 14h15 - EPITA, amphi 4, 24 rue Pasteur, 94270 Le Kremlin-Bicêtre
أعـضاء لجنة المناقـشة :
Javier Esparza,Tech. Univ. München, Germany [Rapporteur]
Radu Mateescu, Inria Grenoble, France, [Rapporteur]
Moshe Y. Vardi, Rice Univ., Houston, Texas, USA, [Rapporteur]
Rüdiger Ehlers, Univ. Bremen, Germany
Stephan Merz, Inria Nancy & Loria, France
Jaco van de Pol, Univ. Twente, Netherlands
Fabrice Kordon, Univ. P.&M. Curie, Paris, France

2 دكـاترة 2014

 Mentions légales
| خـريـطـة المـوقـع