Pierre-Loic Garoche

Research Scientist at Onera - [PGP] View my profile<br />
								on linkedin


courtesy of xkcd.com

Research interests: abstract interpretation, formal verification, theorem provers, symbolic model checking, control software analysis, non linear dynamical systems, convex optimization. Follow @verif_paper on Twitter for related publications.


Most of my papers - including older ones on other topics - are available on DBLP.

Habilitation manuscript (submitted)

Analyzing Lustre models by combining techniques

  • Towards Cooperation of Formal Methods for the Analysis of Critical Control Systems, SAE'11 [DOI]
  • SMT-AI: an Abstract Interpreter as Oracle for k-induction, TAPAS'10 [DOI]
  • Incremental verification with mode variable invariants in state machines, NFM'12 [DOI]
  • Invariant Stream Generators using Automatic Abstract Transformers based on a Decidable Logic, NFM'13 [DOI]
  • A Polynomial Template Abstract Domain based on Bernstein Polynomials, NSV'13, CPSWeek
  • Integrating Policy Iterations in Abstract Interpreters, ATVA'13 [DOI]

  • Formal methods for the analysis of critical control systems models : Combining non-linear and linear analyses. In FMICS'13 [DOI]

  • Formal methods for the analysis of critical control systems models : Combining non-linear and linear analyses. In SAE Int. J. Aerosp. 6(1):150-160, 2013 [DOI]
  • Testing-Based Compiler Validation for Synchronous Languages. NFM'14 [DOI]
  • Computing Quadratic Invariants with Min- and Max-Policy Iterations : a Practical Comparison, FM'14 [DOI]
  • Synthesizing Modular Invariants for Synchronous Code, HSCV'14  [DOI]
  • Automatic Synthesis of Piecewise Linear Quadratic Invariants for Programs, VMCAI'15 [DOI]
  • Compilation of synchronous observers as code contracts, SAC'15 [DOI]
  • Practical policy iterations - A practical use of policy iterations for static analysis: the quadratic case. Formal Methods in System Design 46(2): 163-196 [DOI]
  • Quadratic Zonotopes, An extension of Zonotopes to Quadratic Arithmetics, APLAS'15 - accepted
  • Automatic Synthesis of k-Inductive Piecewise Quadratic Invariants for Switched Affine Control Programs, accepted at Elsevier J. of Computer Languages, Systems and Structures

Analyzing user-domain properties on control systems


Heber Herencia-Zapana (now GE Global Research), Éric Féron (Georgia Tech), Romain Jobredeaux (now Google), Timothy Wang (now UTRC), Sam Owre (SRI), Pierre Roux (Onera), Adrien Champion (Postdoc @ U. Iowa), Rémi Delmas (Onera), Temesghen Kahsai (CMU/NASA), Cesare Tinelli (U. Iowa), Mike Whalen (U. Minnesota), Assalé Adjé (Postdoc @ IRIT), Didier Henrion (LAAS), Alexandre Chapoutot (ENSTA)

Current and past PhD students

  • Pierre Roux 2010-2013: co-advised with Virginie Wiels (ONERA)
    • now at Onera
  • Guillaume Davy 2015-2018?: co-advised with Didier Henrion (LAAS)
  • Simon Duverger 2015-2018?: co-advised with Didier Henrion (LAAS)

Ongoing projects

  • ANR INS CAFÉIN: Combining formal analyses for numerical invariants (PI)

    partners: ONERA (PI), CEA, ENSTA, INRIA, Univ. Perpignan, Prover, Rockwell Collins France
  • ANR ASTRID VORACE: Validation of fast optimization applied to embedded control (coPI)

    partners: IRIT (PI), ONERA, LAAS
  • MoA NASA Ames


Regular teaching at ENSEEIHT and Isae. Occasional at Univ. Tokyo, Univ. of Iowa, Carnegie Mellon.

How to reach me?

My office is located at Onera - Centre de Toulouse, south west of toulouse, near the scientific campus of Rangueil and ISAE (previously Supearo).
You can also try:

    phone +33 (0)5 62 25 29 33,

    fax +33 (0)9 55 35 75 62,

    and (snail) mail

    Onera, Centre Midi-Pyrénées

    BP 74025 -- 2, avenue Édouard Belin

    31055 TOULOUSE CEDEX 4

My email : pierre-loic.garoche@(REMOVE THIS ANTISPAM)onera.fr