Formal Verification of Control System Software published in Princeton Series in Applied Mathematics

@amazon @princeton university press

Previous Next
Pierre-Loïc Garoche

Pierre-Loïc Garoche

Professor of Computer Science

ENAC LII

NASA Ames ARC/TI/RSE

Biography

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.

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

News

Attending CAV 2023 in Paris from July 17th to 22nd
Equation-Directed Axiomatization of Lustre Semantics to Enable Optimized Code Validation, a paper with L. Brun, C. Garion and X. Thirioux accepted at EMSOFT'23
Computation of invariant sets for discrete‐time uncertain systems with E. Khalife, D. Abou Jaoude, and M. Farhood publish in the International Journal of Robust and Nonlinear Control
Participating to Mathworks Research Summit 2023 in Natick, MA on June 22-23rd
Code-Level Formal Verification of Ellipsoidal Invariant Sets for Linear Parameter-Varying Systems with E. Khalife, and M. Farhood presented at NASA Formal Methods 2023 in Houston, TX on May 16-18th
See all

Job offers: summer internships

Ces sujets de stage concernent essentiellement des étudiants et étudiantes avec un bagage en informatique et en contrôle. Connaissance de Matlab Simulink et ou OCaml souhaitée.

Recent Publications

Most publications are available on DBLP, ArXiv, or Google Scholar.

Older publications available through filters.
Céline Bellanger, Pierre-Loic Garoche, Matthieu Martel, Célia Picard (2023). Towards proved formal specification and verification of STL operators as synchronous observers. Submitted.

Dany Abou Jaoude, Pierre-Loic Garoche, Mazen Farhood (2021). Computing State Invariants Using Point-Wise Integral Quadratic Constraints and the S-Procedure. 2021 American Control Conference, ACC 2021, New Orleans, LA, USA, May 26-28, 2021.

Cite

Hamza Bourbouh, Pierre-Loic Garoche, Christophe Garion, Xavier Thirioux (2021). From Lustre to Simulink: reverse compilation for embedded systems applications. ACM Trans. Cyber Phys. Syst..

Cite

Paul Rousse, John Hauser, Pierre-Loic Garoche (2020). A Continuation Method for Computation of H $ınfty$ Gains of Linear Continuous Time Periodic Systems. 2020 59th IEEE Conference on Decision and Control (CDC), Jeju Island, Republic of Korea.

Cite

Paul Rousse, Pierre-Loic Garoche, Didier Henrion (2020). Parabolic set simulation for reachability analysis of linear time-invariant systems with integral quadratic constraint. European Journal of Control.

PDF Cite DOI

See all publications

Collaborators

PhD Students

Avatar

Céline Bellanger

PhD student (2022-)

Avatar

Inès Winandy

PhD student (2023-)

Avatar

Maeva Ongale-Obeyi

Thales Avionics

PhD student (2019-)

Avatar

Wahiba Bachiri

Univ. de Tlemcen, Algeria

PhD student (2021-)

Visitors

Avatar

Dylan Janak

UW

PhD student at UW

Avatar

Danil Berrah

PhD student (2022-)

Avatar

Elias Khalife

Virginia Tech

PhD student

Researchers

Avatar

Célia Picard

Professor at ENAC

Avatar

Matthieu Martel

Professor at Univ. of Perpignan

Avatar

Behçet Açıkmeşe

Professor at Univ. of Washington

Avatar

Alexandre Chapoutot

Professor at ENSTA

Avatar

Christophe Garion

Professor at ISAE-Supaero

Avatar

Xavier Thirioux

Professor at ISAE-Supaero

Avatar

Assalé Adjé

Associate Professor at Univ. of Perpignan

Avatar

Didier Henrion

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

Avatar

Eric Feron

Professor at KAUST (on leave from Georgia Tech)

Avatar

Guillaume Brat

Researcher at NASA Ames

Avatar

Pierre Roux

Researcher at Onera

Alumni

Avatar

Yuanqi Mao

UW

Engineer at Momenta, self-driving vehicle company, Shanghai

Avatar

Hamza Bourbouh

Engineer at Google Zurich

Avatar

Assalé Adjé

Associate Professor at Univ. of Perpignan

Avatar

Sarah Li

ETH

Postdoc

Avatar

Paul Rousse

Engineer at Airbus UpNext

Avatar

Raphael Cohen

ADAS Algorithm Engineer @ Ford (Aptiv)

Avatar

Farah Benmouhoub

ATER Sorbonne Université

Avatar

Guillaume Davy

Formal method Engineer @ Alstom

Avatar

Pierre Roux

Researcher at Onera

Avatar

Arash Sadeghzadeh

Lecturer at Breda University of Applied Sciences, NL

Avatar

Nicolas Nalpon

Researcher at CEA

Projects

.js-id-current_project
Current Projects Past Projects
AItive
Pierre-Loïc Garoche
CAFEIN
Combining Formal Analyses for the Study of Numerical Invariants (ANR INS 2013-2016)
Pierre-Loïc Garoche, Matthieu Martel, Remi Delmas, Alexandre Chapoutot
CAFEIN
Essaim de drones
Swarms of drones (AID 2019-2021)
Pierre-Loïc Garoche, Alexandre Chapoutot, Christophe Garion, Xavier Thirioux
FEANICSES
Formal and Exhaustive Analysis of Numerical Intensive Control Software for Embedded Systems (ANR JCJC 2018-2022)
Pierre-Loïc Garoche
Follow
FEANICSES
SYFI
Synthèse de code en virgule fixe (Région Occitanie 2019-2021)
Pierre-Loïc Garoche, Matthieu Martel, Xavier Thirioux
VORACE
Verified fast optimization for embedded control (ANR ASTRID 2013-2016)
Pierre-Loïc Garoche, Eric Feron, Didier Henrion
Example Project
An example of using the in-built project page.
Slides Follow
Example Project

Tools

CoCoSim: Contract-based Compositional verification of Simulink models
a Matlab Simulink toolbox to support formal specification and verification of Simulink models
Hamza Bourbouh, Pierre-Loïc Garoche
Jul 24, 2015
CoCoSim: Contract-based Compositional verification of Simulink models
OSDP: OCaml Semi Definite Programming
an OCaml library providing interface to SDP/SOS solvers
Pierre Roux, Pierre-Loïc Garoche
Oct 25, 2014
LustreC
a suite of tools to compile and analyze Lustre models
Pierre-Loïc Garoche, Xavier Thirioux, et al
Feb 10, 2013

Teaching

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

System engineering at ENAC: from Requirement engineering to Verification and Validation.

Project tutoring

Probabilistic Swarm Control on Gama (Spring 21)

Probabilistic Swarm Control on Gama (Spring 21)

A team of student is implementing a GUI to interface Markov-based probalistic guidance of swarms into the Gama platform.

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)
  • [sep. 2020] Project meeting SYFI Workshop (Carcassonne, France)
  • [sep. 2020] ESA MBSE Workshop (online)
  • [oct. 2020] Space Agencies (ESA & NASA) G&C V&V Seminar (online)

Contact