Pierre-Loïc Garoche - Personal Website
Equation-Directed Axiomatization of Lustre Semantics to Enable Optimized Code Validation
Research highlights of Communications of the ACM
Formal Verification of Control System Software Princeton Series in Applied Mathematics
Pierre-Loïc Garoche
Professor · ENAC
Pierre-Loïc Garoche is a professor at ENAC, the French National School of Civil Aviation. He was a contractor for NASA Ames in the Robust Software Engineering group from 2013 to 2020 and 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.
Follow @verif_papers on Twitter for related publications.
Interests
- Abstract interpretation
- Formal verification
- Theorem provers & model checking
- Control software analysis
- Non-linear dynamical systems
- Convex optimization
Education
| Habilitation (HDR) | Univ. Toulouse INPT, 2016 |
| PhD, Computer Science | Univ. Toulouse INPT, 2008 |
| MSc, Computer Science | ENS Cachan, 2005 |
| BSc, Math & CS | Univ. Paris Sud Orsay, 2003 |
Recent News
| Date | Title | Description |
|---|---|---|
| Jul 2026 | Elias Khalife is joining the group as a Postdoc | After graduating from Virginia Tech with Prof. Farhood, Elias is joining the group. Welcome Elias! |
| May 2026 | Visit of Prof. Jean-Baptiste Jeannin | Prof. Jean-Baptiste Jeannin from Univ. of Michigan is visiting from 11th-13th of May |
| Jan 2026 | Research highlight in Communications of the ACM | Our EMSOFT paper has been selected as Research Highlight in Jan. edition of C. ACM. |
Publications 2026
Equation-Directed Axiomatization of Lustre Semantics to Enable Optimized Code Validation
Christophe Garion, Lélio Brun, Pierre-Loïc Garoche, Xavier Thirioux
Commun. ACM, vol. 69(1), pp. 93–101, 2026 Journal
DOI BibTeX
@article{DBLP:journals/cacm/GarionBGT26,
doi = {10.1145/3747584},
url = {https://doi.org/10.1145/3747584},
year = {2026},
pages = {93--101},
number = {1},
volume = {69},
journal = {Commun. ACM},
title = {Equation-Directed Axiomatization of Lustre Semantics to Enable Optimized Code Validation},
author = {Christophe Garion and
Lélio Brun and
Pierre-Loïc Garoche and
Xavier Thirioux}
}
Quadratic Characterizations for Reachability Analysis of Neural Networks
Elias Khalife, Mazen Farhood, Pierre-Loic Garoche
2026 Preprint
URL BibTeX
@misc{khalife2026quadraticcharacterizationsreachabilityanalysis,
url = {https://arxiv.org/abs/2605.20482},
primaryclass = {cs.LG},
archiveprefix = {arXiv},
eprint = {2605.20482},
year = {2026},
author = {Elias Khalife and Mazen Farhood and Pierre-Loic Garoche},
title = {Quadratic Characterizations for Reachability Analysis of Neural Networks}
}
Current Projects
CAPOEIRA Embedded Optimization of Complex Attitude Profules, with Airbus Defense and Space (CNES 2025-2026)
CAFEE Control Algorithms Formal End-to-End Verification, with Univ. of Michigan (Prof. Jean-Baptiste Jeannin) (ANR-NSF 2025-2029)
ESA Idea - A New Method to Design, Implement And Verify Optimization Algorithms to Enable their Use Onboard Space Systems (ESA 2026-2029)
Contact
Pierre-Loïc Garoche ENAC — École Nationale de l’Aviation Civile, LII 7, avenue Édouard Belin, 31055 Toulouse, France