Difference between revisions of "Affiche-these-HDR-ADL"

From LRDE

 
Line 6: Line 6:
   
   
<div class="center" style="width: auto; margin-left: auto; margin-right: auto;"><big>'''SOUTENANCE de HDR'''</big>
+
<div class="center" style="width: auto; margin-left: auto; margin-right: auto;"><big>'''SOUTENANCE D'HABILITATION A DIRIGER DES RECHERCHES'''</big>
 
</div>
 
</div>
   
Line 47: Line 47:
 
nonoptimal results (e.g., by using a SAT-solver to find minimal
 
nonoptimal results (e.g., by using a SAT-solver to find minimal
 
deterministic omega-automata of arbitrary acceptance conditions).
 
deterministic omega-automata of arbitrary acceptance conditions).
  +
  +
  +
[https://www.lrde.epita.fr/~adl/dl/adl/duret.17.hdr.pdf Manuscript]
  +
   
 
'''Composition du Jury :'''
 
'''Composition du Jury :'''

Latest revision as of 11:38, 2 February 2017


UPMC.png   Lrde.png   Epita-logo.png  


SOUTENANCE D'HABILITATION A DIRIGER DES RECHERCHES
ALEXANDRE DURET-LUTZ
VENDREDI 10 FEVRIER 2017
A 14H15
Amphi 4
EPITA


Contributions to LTL and ω-automata for Model Checking


Abstract:

We present multiple practical contributions to the automata-theoretic approach to LTL model checking. Most of these contributions are implemented in Spot, 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).


Manuscript


Composition du Jury :

  • 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