Bonjour, J'ai le plaisir de vous inviter à ma soutenance d'habilitation à diriger les recherches, intitulée ``Contributions to LTL and ω-automata for Model Checking'' La soutenance aura lieu le vendredi 10 février à 14h15 à l'Epita dans l'amphi 4 (24 rue Pasteur, 94270 Le Kremlin-Bicêtre). Un plan d'accès est disponible ici: https://www.lrde.epita.fr/~adl/dl/lrde-amphi4.pdf Vous êtes également invités au pot qui suivra, dans la salle alpha du LRDE (2e étage du bâtiment X, 18 rue Pasteur). Le jury sera composé de: 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, examinateur Stephan Merz, Inria Nancy & Loria, France, examinateur Jaco van de Pol, Univ. Twente, Netherlands, examinateur Fabrice Kordon, Univ. P.&M. Curie, Paris, France, examinateur Une version non-définitive du mémoire peut être téléchargée ici: https://www.lrde.epita.fr/~adl/dl/adl/duret.17.hdr.pdf La soutenance aura lieu en anglais, avec le résumé qui suit. 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). -- Alexandre Duret-Lutz