Static Safety for an Actor Dedicated Process Calculus by Abstract Interpretation. - Pierre-Loïc Garoche; Marc Pantel; Xavier Thirioux (FMOODS, 2006)

Accurate Centralization for Applying Model Checking on Networked Applications. - Cyrille Artho; Pierre-Loïc Garoche (ASE, 2006)

Adaptive Geographically Bound Mobile Agents. - Kenji Tei; Christian Sommer 001; Yoshiaki Fukazawa; Shinichi Honiden; Pierre-Loïc Garoche (MSN, 2006)

A Property-Driven Approach to Formal Verification of Process Models. - Benoît Combemale; Xavier Crégut; Pierre-Loïc Garoche; Xavier Thirioux; François Vernadat 001 (ICEIS (Selected Papers), 2007)

Towards a Formal Verification of Process Model's Properties SIMPLEPDL and TOCL Case Study. - Benoît Combemale; Pierre-Loïc Garoche; Xavier Crégut; Xavier Thirioux; François Vernadat 001 (ICEIS (3), 2007)

Abstract Interpretation-based Static Safety for Actors. - Pierre-Loïc Garoche; Marc Pantel; Xavier Thirioux (J. Softw., 2007)

Static Analysis of an Actor-based Process Calculus by Abstract Interpretation. (Analyse statique d'un calcul d'acteurs par interprétation abstraite). - Pierre-Loïc Garoche (2008)

Essay on Semantics Definition in MDE - An Instrumented Approach for Model Verification. - Benoît Combemale; Xavier Crégut; Pierre-Loïc Garoche; Xavier Thirioux (J. Softw., 2009)

SMT-AI: an Abstract Interpreter as Oracle for k-induction. - Pierre Roux 001; Remi Delmas; Pierre-Loïc Garoche (TAPAS@SAS, 2010)

A generic ellipsoid abstract domain for linear time invariant systems. - Pierre Roux 001; Romain Jobredeaux; Pierre-Loïc Garoche; Eric Feron (HSCC, 2012)

PVS Linear Algebra Libraries for Verification of Control Software Algorithms in C/ACSL. - Heber Herencia-Zapana; Romain Jobredeaux; Sam Owre; Pierre-Loïc Garoche; Eric Feron; Gilberto Pérez 001; Pablo Ascariz (NASA Formal Methods, 2012)

Incremental Verification with Mode Variable Invariants in State Machines. - Temesghen Kahsai; Pierre-Loïc Garoche; Cesare Tinelli; Mike Whalen (NASA Formal Methods, 2012)

Invariant stream generators using automatic abstract transformers based on a decidable logic - Pierre-Loïc Garoche; Temesghen Kahsai; Cesare Tinelli (CoRR, 2012)

Integrating Policy Iterations in Abstract Interpreters. - Pierre Roux 001; Pierre-Loïc Garoche (ATVA, 2013)

Formal Methods for the Analysis of Critical Control Systems Models: Combining Non-linear and Linear Analyses. - Adrien Champion; Rémi Delmas; Michael Dierkes; Pierre-Loïc Garoche; Romain Jobredeaux; Pierre Roux 001 (FMICS, 2013)

Incremental Invariant Generation Using Logic-Based Automatic Abstract Transformers. - Pierre-Loïc Garoche; Temesghen Kahsai; Cesare Tinelli (NASA Formal Methods, 2013)

From Design to Implementation: an Automated, Credible Autocoding Chain for Control Systems. - Timothy Wang; Romain Jobredeaux; Heber Herencia-Zapana; Pierre-Loïc Garoche; Arnaud Dieumegard; Eric Feron; Marc Pantel (CoRR, 2013)

Computing Quadratic Invariants with Min- and Max-Policy Iterations: A Practical Comparison. - Pierre Roux 001; Pierre-Loïc Garoche (FM, 2014)

Testing-Based Compiler Validation for Synchronous Languages. - Pierre-Loïc Garoche; Falk Howar; Temesghen Kahsai; Xavier Thirioux (NASA Formal Methods, 2014)

Synthesizing Modular Invariants for Synchronous Code. - Pierre-Loïc Garoche; Arie Gurfinkel; Temesghen Kahsai (HCVS, 2014)

Credible Autocoding of Convex Optimization Algorithms. - Timothy Wang; Romain Jobredeaux; Marc Pantel; Pierre-Loïc Garoche; Eric Feron; Didier Henrion (CoRR, 2014)

Quadratic Zonotopes - An Extension of Zonotopes to Quadratic Arithmetics. - Assalé Adjé; Pierre-Loïc Garoche; Alexis Werey (APLAS, 2015)

Closed loop analysis of control command software. - Pierre Roux 001; Romain Jobredeaux; Pierre-Loïc Garoche (HSCC, 2015)

Compilation of synchronous observers as code contracts. - Arnaud Dieumegard; Pierre-Loïc Garoche; Temesghen Kahsai; Alice Taillar; Xavier Thirioux (SAC, 2015)

Property-based Polynomial Invariant Generation Using Sums-of-Squares Optimization. - Assalé Adjé; Pierre-Loïc Garoche; Victor Magron (SAS, 2015)

Automatic Synthesis of Piecewise Linear Quadratic Invariants for Programs. - Assalé Adjé; Pierre-Loïc Garoche (VMCAI, 2015)

A Sums-of-Squares Extension of Policy Iterations. - Assalé Adjé; Pierre-Loïc Garoche; Victor Magron (CoRR, 2015)

Practical policy iterations - A practical use of policy iterations for static analysis: the quadratic case. - Pierre Roux 001; Pierre-Loïc Garoche (Formal Methods Syst. Des., 2015)

Convex Optimization-based Static Analysis for Control Systems. (Analyse statique de contrôleurs à base d'optimisation convexe). - Pierre-Loïc Garoche (2016)

Formal Analysis of Robustness at Model and Code Level. - Timothy E. Wang; Pierre-Loïc Garoche; Pierre Roux 001; Romain Jobredeaux; Eric Feron (HSCC, 2016)

Hierarchical State Machines as Modular Horn Clauses. - Pierre-Loïc Garoche; Temesghen Kahsai; Xavier Thirioux (HCVS@ETAPS, 2016)

Automated analysis of Stateflow models. - Hamza Bourbouh; Pierre-Loïc Garoche; Christophe Garion; Arie Gurfinkel; Temesghen Kahsai; Xavier Thirioux (LPAR, 2017)

Automatic synthesis of k-inductive piecewise quadratic invariants for switched affine control programs. - Assalé Adjé; Pierre-Loïc Garoche (Comput. Lang. Syst. Struct., 2017)

Foundations of Intelligent Additive Manufacturing. - Kévin Garanger; Eric Feron; Pierre-Loïc Garoche; Julian J. Rimoli; John D. Berrigan; Martha A. Grover; Kerianne Hobbs (CoRR, 2017)

Credible Autocoding of The Ellipsoid Algorithm Solving Second-Order Cone Programs. - Raphael Cohen; Eric Feron; Pierre-Loïc Garoche (CDC, 2018)

Preserving Functional Correctness of Cyber-Physical System Controllers: From Model to Code. - Guillaume Davy; Christophe Garion; Pierre-Loïc Garoche; Pierre Roux 001; Xavier Thirioux (FDL, 2018)

Experiments in Verification of Linear Model Predictive Control: Automatic Generation and Formal Verification of an Interior Point Method Algorithm. - Guillaume Davy; Eric Feron; Pierre-Loïc Garoche; Didier Henrion (LPAR, 2018)

Formal verification of an interior point algorithm instanciation. - Guillaume Davy; Eric Feron; Pierre-Loïc Garoche; Didier Henrion (CoRR, 2018)

Guaranteed Simulation of Dynamical Systems with Integral Constraints and Application on Delayed Dynamical Systems. - Paul Rousse; Julien Alexandre Dit Sandretto; Alexandre Chapoutot; Pierre-Loïc Garoche (CyPhy/WESE, 2019)

Parabolic Set Simulation for Reachability Analysis of Linear Time Invariant Systems with Integral Quadratic Constraint. - Paul Rousse; Pierre-Loïc Garoche; Didier Henrion (ECC, 2019)

Semidefinite Approximations of Reachable Sets for Discrete-time Polynomial Systems. - Victor Magron; Pierre-Loïc Garoche; Didier Henrion; Xavier Thirioux (SIAM J. Control. Optim., 2019)

A Continuation Method for computation of H∞ gains of Linear Continuous-Time Periodic Systems. - Paul Rousse; John Hauser; Pierre-Loïc Garoche (CDC, 2020)

The Ten Lockheed Martin Cyber-Physical Challenges: Formalized, Analyzed, and Explained. - Anastasia Mavridou; Hamza Bourbouh; Dimitra Giannakopoulou; Thomas Pressburger; Mohammad Hejase; Pierre-Loïc Garoche; Johann Schumann (RE, 2020)

Bridging the Gap Between Requirements and Simulink Model Analysis. - Anastasia Mavridou; Hamza Bourbouh; Pierre-Loïc Garoche; Dimitra Giannakopoulou; Thomas Pressburger; Johann Schumann (REFSQ Workshops, 2020)

Fixed Points of the Set-Based Bellman Operator. - Sarah H. Q. Li; Assalé Adjé; Pierre-Loïc Garoche; Behçet Açikmese (CoRR, 2020)

Verification and Validation of Convex Optimization Algorithms for Model Predictive Control. - Raphael Cohen; Eric Feron; Pierre-Loïc Garoche (J. Aerosp. Inf. Syst., 2020)

Computing State Invariants Using Point-Wise Integral Quadratic Constraints and the S-procedure. - Dany Abou Jaoude; Pierre-Loïc Garoche; Mazen Farhood (ACC, 2021)

Parallel Accurate and Reproducible Summation. - Farah Benmouhoub; Pierre-Loïc Garoche; Matthieu Martel (SAI (1), 2021)

An Efficient Summation Algorithm for the Accuracy, Convergence and Reproducibility of Parallel Numerical Methods. - Farah Benmouhoub; Pierre-Loïc Garoche; Matthieu Martel (VSTTE, 2021)

Bounding fixed points of set-based Bellman operator and Nash equilibria of stochastic games. - Sarah H. Q. Li; Assalé Adjé; Pierre-Loïc Garoche; Behçet Açikmese (Autom., 2021)

From Lustre to Simulink: Reverse Compilation for Embedded Systems Applications. - Hamza Bourbouh; Pierre-Loïc Garoche; Christophe Garion; Xavier Thirioux (ACM Trans. Cyber Phys. Syst., 2021)

Reachability Set Analysis of Closed-Loop Nonlinear Systems with Neural Network Controllers. - Arash Sadeghzadeh; Pierre-Loïc Garoche (ACC, 2022)

Reachability Analysis of Linear Parameter-Varying Systems with Neural Network Controllers. - Arash Sadeghzadeh; Pierre-Loïc Garoche (CCTA, 2022)

Successive Convexification for Optimal Control with Signal Temporal Logic Specifications. - Yuanqi Mao; Behçet Açikmese; Pierre-Loïc Garoche; Alexandre Chapoutot (HSCC, 2022)

Set-based value operators for non-stationary Markovian environments. - Sarah H. Q. Li; Assalé Adjé; Pierre-Loïc Garoche; Behçet Açikmese (CoRR, 2022)

Reducing Collision Risk in Multi-Agent Path Planning: Application to Air traffic Management. - Sarah H. Q. Li; Avi Mittal; Pierre-Loïc Garoche; Behçet Açikmese (CoRR, 2022)

Exact Computation of Maximal Invariant Sets for Safe Markov Chains - Lattice Theoretic Approach. - Dylan Janak; Pierre-Loïc Garoche; Behçet Açikmese (IEEE Trans. Autom. Control., 2022)

Code-Level Formal Verification of Ellipsoidal Invariant Sets for Linear Parameter-Varying Systems. - Elias Khalife; Pierre-Loïc Garoche; Mazen Farhood (NFM, 2023)

Towards Proved Formal Specification and Verification of STL Operators as Synchronous Observers. - Céline Bellanger; Pierre-Loïc Garoche; Matthieu Martel; Célia Picard (FMAS@iFM, 2023)

Equation-Directed Axiomatization of Lustre Semantics to Enable Optimized Code Validation. - Lélio Brun; Christophe Garion; Pierre-Loïc Garoche; Xavier Thirioux (ACM Trans. Embed. Comput. Syst., 2023)

SCvxPyGen: Autocoding SCvx Algorithm. - Danil Berrah; Alexandre Chapoutot; Pierre-Loïc Garoche (CDC, 2024)

Formally Proving Invariant Systemic Properties of Control Programs Using Ghost Code and Integral Quadratic Constraints. - Elias Khalife; Pierre-Loïc Garoche; Mazen Farhood (NFM, 2025)

Set-based value operators for non-stationary and uncertain Markov decision processes. - Sarah H. Q. Li; Assalé Adjé; Pierre-Loïc Garoche; Behçet Açikmese (Autom., 2025)

Automated Fixed-Point Precision Optimization for FPGA Synthesis. - Inès Winandy; Arnaud Dion; Florent Manni; Pierre-Loïc Garoche; Dorra Ben Khalifa; Matthieu Martel (IEEE Open J. Circuits Syst., 2025)

Formal specification and SMT verification of quantized neural network for autonomous vehicles. - Wahiba Bachiri; Yassamine Seladji; Pierre-Loïc Garoche (Sci. Comput. Program., 2025)

Formally proved specification of non-nested STL formulas as synchronous observers. - Céline Bellanger; Pierre-Loïc Garoche; Matthieu Martel; Célia Picard (Sci. Comput. Program., 2025)