Avatar

Pierre-loic Garoche

Senior Research Scientist in Formal Verification

Onera DTIS/COVNI

NASA Ames ARC/TI/RSE

Biography

Pierre-Loïc Garoche is a senior research scientist at Onera, the French Aerospace Lab and a contractor for NASA Ames in the Robust Software Engineering group.

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.

Interests

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

Education

  • 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

Collaborators

PhD Students

Avatar

Hamza Bourbouh

PhD student (2017-)

Avatar

Farah Benmouhoub

PhD student (2018-)

Avatar

Paul Rousse

PhD student (2016-)

Researchers

Avatar

Alexandre Chapoutot

Professor at ENSTA

Avatar

Christophe Garion

Professor at ISAE-Supaero

Avatar

Didier Henrion

Senior Researcher (Directeur de Recherche) at LAAS-CNRS and Professor at Prague University

Avatar

Eric Feron

Professor at Georgia Tech

Avatar

Matthieu Martel

Professor at Univ. of Perpignan

Avatar

Pierre Roux

Researcher at Onera

Avatar

Remi Delmas

Researcher at ONERA

Avatar

Xavier Thirioux

Associate Professor at INPT/IRIT

Avatar

Assalé Adjé

Associate Professor at Univ. of Perpignan

Avatar

Behçet Açıkmeşe

Professor at Univ. of Washington

Avatar

Guillaume Brat

Researcher at NASA Ames

Alumni

Avatar

Pierre Roux

Researcher at Onera

Avatar

Guillaume Davy

Formal method Engineer @ Alstom

Avatar

Assalé Adjé

Associate Professor at Univ. of Perpignan

Avatar

Raphael Cohen

ADAS Algorithm Engineer @ Aptiv

Projects

.js-id-current_project

CAFEIN

Combining Formal Analyses for the Study of Numerical Invariants (ANR INS 2013-2016)

FEANICSES

Formal and Exhaustive Analysis of Numerical Intensive Control Software for Embedded Systems (ANR JCJC 2018-2022)

SYFI

Synthèse de code en virgule fixe (Région Occitanie 2019-2021)

VORACE

Verified fast optimization for embedded control (ANR ASTRID 2013-2016)

Tools

CoCoSim: Contract-based Compositional verification of Simulink models

a Matlab Simulink toolbox to support formal specification and verification of Simulink models

LustreC

a suite of tools to compile and analyze Lustre models

OSDP: OCaml Semi Definite Programming

an OCaml library providing interface to SDP/SOS solvers

Teaching

Regular teaching at ISAE-Supaero and INPT-ENSEEIHT in Toulouse, mainly on formal methods and abstract interpretation

Talks & Seminars

2005

  • [jan. 2005] Semantic and Abstract Interpretation Seminar (ENS Ulm, Paris)

2006

  • [feb. 2006] Tokyo Programming Seminar (Tokyo University)
  • [feb. 2006] Honiden Laboratory Student Seminar (National Institute of Informatics, Tokyo)

2007

  • [dec. 2007] Verification Seminar (LIAFA, Université Paris 7)

2008

  • [jan. 2008] Informatics and Mathematical Modelling (DTU, Lyngby, Denmark)
  • [feb. 2008] Seminar of PPS/X/MeASI Team (LiX – CEA, Palaiseau)

2010

  • [dec. 2010] Airbus Formal Methods Workshop (Airbus Operation SAS, Toulouse)
  • [july 2010] DALI Team Seminar (ELIAUS, Université of Perpignan)

2011

  • [mar. 2011] Seminar of PPS/X/MeASI Team (LiX – CEA, Palaiseau)
  • [mar. 2011] GRACE Seminar on Advanced Software Science and Engineering\(National Institute of Informatics, Tokyo, Japan)
  • [mar. 2011] Collaborative Research Team for Verification Seminar (AIST Kobe, Japan)

2012

  • [feb. 2012] NASA Ames (Moffett field, CA, USA)
  • [feb. 2012] U. of Iowa Computer Science Dpt Colloquium (Iowa City, IA, USA)
  • [avr. 2012] NASA Langley (Hampton, VA, USA)
  • [avr. 2012] CMACS Seminar - Carnegie Mellon University (Pittsburgh PA, USA)
  • [oct. 2012] Invited speaker at FMCAD'12 (tutorial session, Cambridge, UK)
  • [oct. 2012] Seminar at IRISA INRIA-CNRS, Rennes

2013

  • [jan. 2013] LIST Seminar (CEA, Palaiseau, France)
  • [apr. 2013] Journée FAC – Formalisation des activités concurrentes (Toulouse, France)
  • [apr. 2013] Invited speaker at OBEO Roadshow (Toulouse, France)
  • [may 2013] Seminar at ENSTA-Paristech (Palaiseau, France)
  • [june 2013] Stanford Department of Aeronautics and Astronautics Seminar (Stanford, CA, USA)
  • [june 2013] Keynote at Control Software Verification Workshop CSVW (Moffett Field, CA, USA)
  • [july 2013] SRI International (Menlo Park, CA, USA)
  • [dec. 2013] Keynote and organization of Aerospace 2050, in honor of Marc Pelegrin 90th birthday (Toulouse, France)

2015

  • [mar. 2015] Invited speaker at NSF project SORTIES 1st workshop (Boulder, CO, USA)
  • [apr. 2015] Invited speaker at GT Shy – Groupe de Travail Système HYbride of DigiCosme Labex (Palaiseau, France)
  • [oct. 2015] Kestrel Institute (Palo Alto, CA, USA)
  • [oct. 2015] SRI International (Menlo Park, CA, USA)
  • [oct. 2015] NASA Ames (Moffett field, CA, USA)
  • [oct. 2015] United Tech Research Center (Berkeley, CA)

2016

  • [mar. 2016] Invited speaker at NSF project SORTIES 2nd workshop (Boulder, CO, USA)
  • [may 2016] United Tech Research Center (Cork, Irelande)
  • [june 2016] Keynote speaker at CEA FramaC days
  • [july 2016] NASA Langley (Hampton, VA, USA), séminaire commun aux équipes informatiques et automatiques
  • [july 2016] Univ. of Minnesota, Software Engineering Center (UMSEC), Minneapolis, MN, USA
  • [july 2016] Univ. of Michigan (Ann Arbor, MI), Dpt. of Aerospace
  • [july 2016] Toyota Technical Center (Ann Arbor, MI, USA)
  • [nov. 2016] INRIA Sophia-Antipolis, Séminaire de l'équipe McTAO
  • [nov. 2016] IMT Lucca, (Lucca, Italie)
  • [nov. 2016] United Tech Research Center (East Hartford, CT, USA)

2017

  • [feb. 2017] Univ. Technique de Prague, Tchéquie
  • [june 2017] Price Induction (Anglet)
  • [june 2017] SRI International (Menlo Park, CA, USA)
  • [oct. 2017] Ales – UTRC Italy (Rome, Italie)
  • [nov. 2017] RSE seminar, NASA Ames (Moffett field, CA, USA)
  • [dec. 2017] Groupe de travail VS-CPS Vérification et Synthèse de Systèmes Cyber-Physiques

2018

  • [mar. 2018] University of Washington, Aeronautics and Astronautics Dpt, Seattle, WA, USA
  • [mar. 2018] United Tech Research Center (Berkeley, CA)
  • [june 2018] Invited speaker at Nonlinear and Computational Control: A Workshop to Honor Prof. John Hauser on his 60th Birthday (Milwaukee, WI, USA)
  • [july 2018] Invited speaker at Numerical Software Verification, a FloC event (Oxford, UK)
  • [sep. 2018] Invited speaker at the Forum on specification & Design Languages, special session on Logic and Mathematics behind Design Automation (Munich, Allemagne)
  • [oct. 2018] Adacore (Paris, France)

2019

  • [mar. 2019] Univ. of Colorado Boulder (Boulder, CO, USA)
  • [june 2019, 68NQRT Seminar of INRIA Rennes (Rennes, France)
  • [june 2019] Project meeting AID Swarms of Drones project (ISAE, Toulouse, France)
  • [nov. 2019] Project meeting AID Swarms of Drones project (Polytechnique, Palaiseau, France)
  • [nov. 2019] Meeting with DLR (Deutsches Zentrum für Luft- und Raumfahrt) (Onera, Palaiseau, France)

2020

  • [jan 2020] RSE seminar, NASA Ames (Moffett field, CA, USA)

Contact