Formal Methods and Verification at ULB   Computer Science Department at ULB  

Tristan Le Gall

I'm a Post-Doc researcher at ULB in the Verification team within the European Moves project.

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

Building: N.O., Office: N8.207
Phone: +32 2 650.58.57, Fax: +32 2 650.56.09
Email: tlegall at ulb dot ac dot be



Research Interests

  • Abstract Interpretation
  • Model Checking of Infinite Systems
  • Supervisory Control of Discrete Event Systems
  • Game Theory


  • Publications

    Journals

  • [2006] T. Le Gall, B. Jeannet and H. Marchand. Contrôle de systèmes symboliques, discrets ou hybrides, Technique et Science Informatiques (TSI), 25:293-319, 2006. (more)
  • [2010] G. Kalyon, Le Gall T, H. Marchand and T. Massart. Decentralized Control of Infinite Systems, submitted to Journal of Discrete Event Systems
  • [2010] G. Kalyon, Le Gall T, H. Marchand and T. Massart. Covering-Based Supervisory Control of Infinite Symbolic Transition Systems under Partial Observation, submitted to Journal of Discrete Event Systems

    Conferences

  • [2010] E. Filiot, T. Le Gall and J-F. Raskin. Iterated Regret Minimization in Game Graphs. Accepted to MFCS'10. Preliminary version.
  • [2010] G. Geeraerts, G. Kalyon, N. Maquet, T. Le Gall and J.-F. Raskin. Lattice-Valued Binary Decision Diagrams. Accepted to ATVA'10
  • [2009] G. Kalyon, T. Le Gall, H. Marchand and T. Massart. Computational Complexity for State-Feedback Controllers with Partial Observation, in 7th International Conference on Control and Automation, ICCA'09, Christchurch, New Zealand, December 2009. (more)
  • [2009] G. Kalyon, T. Le Gall, H. Marchand and T. Massart. Contrôle décentralisé de systèmes symboliques infinis sous observation partielle, in 7ème Colloque Francophone sur la Modélisation des Systèmes Réactifs, Nantes, France, november 2009. (more)
  • [2009] G. Kalyon, Le Gall T, H. Marchand and T. Massart. Control of Infinite Symbolic Transition Systems under Partial Observation, in European Control Conference, Budapest, Hungary, August 2009. (more)
  • [2009] A. Heussner, T. Le Gall, and G. Sutre. Extrapolation-based Path Invariants for Abstraction Refinement of Fifo Systems. In Proc. 16th Int. SPIN Workshop on Model Checking of Software (SPIN'09), Grenoble, France, Jun. 2009, volume 5578 of Lecture Notes in Computer Science, pages 107-124. Springer, 2009
  • [2007] T. Le Gall and B. Jeannet. Lattice automata: a representation of languages over an infinite alphabet, and some applications to verification, in The 14th International Static Analysis Symposium, SAS 2007, Kongens Lyngby, Denmark, August 2007. (more)
  • [2006] T. Le Gall, B. Jeannet, and T. Jéron. Verification of Communication Protocols using Abstract Interpretation of FIFO queues, in 11th International Conference on Algebraic Methodology and Software Technology, AMAST '06, Kuressaare, Estonia, Michael Johnson, Varmo Vene (eds.), Volume 4019, July 2006. (more)
  • [2005] T. Le Gall, B. Jeannet and H. Marchand. Supervisory Control of Infinite Symbolic Systems using Abstract Interpretation, in 44nd IEEE Conference on Decision and Control (CDC'05) and Control and European Control Conference ECC 2005, Pages 31-35, Seville (Spain), December 2005. (more)

    Thesis

  • [2008] Ph.D. Thesis (in English) Abstract Lattices for the Verification of Systems with Stacks and Queues.


  • Tools

  • an OCaml Library for Lattice Automata
  • a static analyzer for Symbolic Communicating Machines
  • McScM: a model checker for Symbolic Communicating Machines
  • SMACS: a tool for the supervisory control of infinite systems under partial observation