Pierre-loic Garoche

Senior Research Scientist in Formal Verification



Pierre-Loïc Garoche is a professor at ENAC, the French National School of Civil Aviation, and a contractor for NASA Ames in the Robust Software Engineering group. He was a senior research scientist at Onera, the French Aerospace Lab from 2008 to 2020.

His work is in the field of Software Verification, between theory and applications, mainly focused on the use of formal methods in critical embedded systems development, in a certified context. His primary interest is at the frontier between academy and industry, studying the application of formal methods on numerical intensive control systems software such as aircraft controllers, satellite attitude and orbital control systems, or trajectory planning algorithms for drones and rocket pinpoint landing.

His objective is to validate and develop methods to automatically verify critical embedded software, either at code level or at model level.

Follow @verif_paper on Twitter for related publications.


  • abstract interpretation
  • formal verification
  • theorem provers
  • symbolic model checking
  • control software analysis
  • non linear dynamical systems
  • convex optimization
  • verification of numerical algorithms


  • Habilitation à Diriger des Recherches, 2016

    University of Toulouse (INPT)

  • PhD in Computer Science, 2008

    University of Toulouse (INPT)

  • MSc in Computer Science, 2005

    École Normale Supérieure de Cachan

  • BSc in Math and CS, 2003

    Univ. Paris Sud Orsay