Formal Methods and Verification at ULB   Computer Science Department at ULB  

Emmanuel Filiot

From October to December 2011, I'm visiting Professor Rajeev Alur at University of Pennsylvania.

Ph.D., INRIA Lille (France), 2008.

I'm a Post-Doc researcher at ULB in the Move team within the European Gasics project. My post-doc is funded by FNRS.

Département d'Informatique
Université Libre de Bruxelles
Bld du Triomphe CP 212
1050 Brussels, Belgium

Building: N.O., Office: N8.110
Phone: +32 2 650.64.64, Fax: +32 2 650.56.09
Email: efiliot at ulb dot ac dot be


Research Interests

  • Temporal Logics
  • Game Theory for Synthesis
  • Logics and Automata for Infinite and Finite Words and Trees
  • Tree Transformations
  • XML Databases

  • Publications

    Recent Work

  • [2011] Acacia+, a tool for LTL synthesis. A. Bohy, V. Bruyère, E. Filiot, N. Jin, J.-F. Raskin. Submitted. Try Acacia+ Online!
  • [2011] Quantitative Languages Defined by Functional Automata. E. Filiot, R. Gentilini, J.-F. Raskin. Submitted.
  • [2011] Visibly Pushdown Transducers with Look-Ahead. E. Filiot, F. Servais. To appear in SOFSEM'12.
  • [2011] Streamability of Nested Word Transductions. E. Filiot, O. Gauwin, P.-A. Reynier, F. Servais. To appear in FSTTCS'11.
  • Journals

  • [2011] Antichains and Compositional Algorithms for LTL Synthesis. E. Filiot, N. Jin and J.-F. Raskin. Extended version of the CAV'09 and ATVA'10 papers. Journal of Formal Methods in System Design. To appear. Springer link.
  • [2011] Exploiting Structure in LTL Synthesis. E. Filiot, N. Jin and J.-F. Raskin. Invited for publication in International Journal on Software Tools for Technology Transfer. To appear.
  • [2010] Tree Automata with Global Constraints. E. Filiot, Jean-Marc Talbot and Sophie Tison. Invited version of DLT'08. Published in International Journal of Foundations of Computer Science, Volume 21, Issue 4.
  • International Conferences

  • [2011] Visibly Pushdown Transducers with Look-Ahead. E. Filiot, F. Servais. To appear in SOFSEM'12.
  • [2011] Streamability of Nested Word Transductions. E. Filiot, O. Gauwin, P.-A. Reynier, F. Servais. To appear in FSTTCS'11.
  • [2010] Compositional Algorithms for LTL Synthesis. E. Filiot, J. Naiyong and J.-F. Raskin. To appear in International Symposium on Automated Technology for Verification and Analysis (ATVA'10).
  • [2010] Properties of Visibly Pushdown Transducers.. E. Filiot, J.-F. Raskin, P-A. Reynier, F. Servais and J.-M. Talbot. To appear in 35th International Symposium on Mathematical Foundations of Computer Science (MFCS'10).
  • [2010] Iterated Regret Minimization in Game Graphs. E. Filiot, T. Le Gall and J-F. Raskin. To appear in 35th International Symposium on Mathematical Foundations of Computer Science (MFCS'10). Full version.
  • [2010] Efficient Enumeration for Conjunctive Queries over X-underbar Structures. G. Bagan, A. Durand, E. Filiot and O. Gauwin. To appear in Computer Science Logic (CSL'10).
  • [2009] An Antichain Algorithm for LTL Realizability. E. Filiot, Jin Naiyong and Jean-François Raskin. Accepted to CAV. Invited for publication inf Journal of Formal Methods in System Design.
  • [2008] Tree Automata with Global Constraints. E. Filiot, Jean-Marc Talbot and Sophie Tison. Accepted to DLT. Invited for publication to International Journal of Foundations of Computer Science.
  • [2008] Regular n-ary queries in trees and variable independence. E. Filiot and S. Tison. Accepted to IFIP TCS.
  • [2007] Polynomial Time Fragments of XPath with Variables . E. Filiot, J. Niehren, J.-M. Talbot and S. Tison. Accepted to ACM SIGMOD/PODS'07 International Conference.
  • [2007] Satisfiability of a Spatial Logic with Tree Variables. E. Filiot, J.-M. Talbot and S. Tison. Accepted to the 16th EACSL Annual Conference on Computer Science and Logic (CSL).
  • Workshops

  • [2010] Regret Minimization in Game Graphs, Workshop on Timed and Infinite Systems. Warwick University, UK.
  • [2009] An Antichain Algorithm for LTL Realizability, GAMES'09: Annual Workshop of the ESF Networking Programme on Games for Design and Verification. slides.
  • [2008] Querying Regular Sets of XML Documents, S. Staworko, E. Filiot, J. Chomicki, Logic in Databases Workshop.
  • [2006] Composing Monadic Queries in Trees . E. Filiot, J. Niehren, J.-M. Talbot and S. Tison, , PLAN-X'06, USA.
  • Technical Reports

  • [2010] On Functionality of Visibly Pushdown Transducers. E. Filiot, J.-F. Raskin, P-A. Reynier, F. Servais and J.-M. Talbot. Technical Report.
  • Thesis

  • [2008] Ph.D. Thesis (in English) Logics for n-ary queries in trees.
  • [2005] Master's Thesis (in French) Composition de requêtes monadiques dans les arbres
  • Tools

  • Acacia+. A tool for LTL synthesis. Try it online!
  • Tree automata libraries for OCaml. No longer maintained.
  • Misc

  • Moves newsletter, workpackage 7, Incremental design and verification, 2010.

    Talks

  • [2011] Height-Bounded Memory Visibly Pushdown Transductions. CFV Meeting.
  • [2011] Antichains and Compositional Algorithms for LTL Synthesis. CFV Meeting.
  • [2010] Compositional Algorithms for LTL Synthesis. Gasics Meeting (Aalborg), Move team seminar, ULB, ATVA'10.
  • [2010] Iterated Regret Minimization in Game Graphs. Gasics Meeting (Aalborg), Move team seminar, ULB, MFCS'10.
  • [2009] Towards Efficient Synthesis of LTL Specifications. FNRS Contact Group on Fundamental Computer Science, Annual Meeting. slides.
  • [2009,2010] An antichain algorithm for LTL Realizability, Quasimodo and Gasics Meetings (ULB), LIAFA seminar (Paris 7), Mostrare seminar (Lille), Logic team of Paris 7, GAMES'09 workshop.
  • [2009] Tutorial on Determinization of Büchi Automata, Move team seminar, ULB. slides
  • [2008] Tree automata with global constraints, DLT'08, Kyoto slides.
  • [2008] Regular n-ary queries and variable independence, MOSTRARE seminar and IFIP TCS'08, Milano slides.
  • [2008] Polynomial-time fragments of XPath with Variables, ANR project ENUM, Paris.
  • [2008] Information Extraction, Eurodoc'08, Lille.
  • [2007] TQL logic Centre Federe en Verification, Bruxelles.
  • [2007] Satisfiability of a Spatial Logic with Tree Variables CSL, Lausanne. slides
  • [2007] Satisfiability of a Spatial Logic with Tree Variables, in Mostrare seminar (Lille), LIF (Marseille) and Paris 1.
  • [2007] Poynomial Time Fragments of XPath with Tree Variables, Mostrare seminar (Lille) and PODS'07 (Beijing).
  • [2006] Composing Monadic Queries in Trees, PLAN-X Workshop, Charleston, USA.
  • [2006] Binary query composition and application to XPath, TraLaLA (XML Transformation Languages: logic and applications), Marseille.
  • [2005] Composition de requetes monadiques dans les arbres, TraLaLA (XML Transformation Languages: logic and applications), Lille. (in french)
  • [2005] Composition of monadic queries in trees, Mostrare seminar, Lille.

    Teaching (in french)

    Teaching (in French)

  • 2009-2010, 2010-2011, Bachelier 3: Logique Informatique . Université Libre de Bruxelles et Ecole Polytechnique de Bruxelles. Cours, exercices et projets.
  • 2006-2007, Master 1: Fouille de données
    Sujet TP Clustering de Couleurs (utilisation de méthodes de clustering pour transformer une image en une image avec moins de couleurs). Pour les sources, me contacter par email.
  • 2006-2007, Master 1: Algorithmique Avancée et Complexité (voir le portail)
    Sujet TP programmation dynamique: un chameau dans le désert
  • 2005-2006, Master 1: Algorithmique Avancée et Complexité (voir la page de Sophie Tison)
  • 2003-2004, Initiation à l'informatique, utilisation de Maple, classes préparatoires (PCSI) au lycée La Martinière (Lyon)
  • Divers

  • Un début d'introduction à Objective Caml avec un peu de code. Pour plus d'infos: le site officiel, et l'excellent cours de programmation de Daniel Hirschkoff.