Pierre-Loïc Garoche

77 papers A* 1A 1B 7C 4Misc 1Journal 34Unranked 27

Year	Rank	Type	Title / Venue / Authors
2026	J	`jnl`	Equation-Directed Axiomatization of Lustre Semantics to Enable Optimized Code Validation. Commun. ACM Christophe Garion, Lélio Brun, Pierre-Loïc Garoche, Xavier Thirioux
2025	J	`jnl`	Automated Fixed-Point Precision Optimization for FPGA Synthesis. IEEE Open J. Circuits Syst. Inès Winandy, Arnaud Dion, Florent Manni, Pierre-Loïc Garoche, Dorra Ben Khalifa, Matthieu Martel
2025	J	`jnl`	Formal specification and SMT verification of quantized neural network for autonomous vehicles. Sci. Comput. Program. Wahiba Bachiri, Yassamine Seladji, Pierre-Loïc Garoche
2025	—	`conf`	Formally Proving Invariant Systemic Properties of Control Programs Using Ghost Code and Integral Quadratic Constraints. NFM Elias Khalife, Pierre-Loïc Garoche, Mazen Farhood
2025	J	`jnl`	Formally Proving Invariant Systemic Properties of Control Programs Using Ghost Code and Integral Quadratic Constraints. CoRR Elias Khalife, Pierre-Loïc Garoche, Mazen Farhood
2025	J	`jnl`	Formally proved specification of non-nested STL formulas as synchronous observers. Sci. Comput. Program. Céline Bellanger, Pierre-Loïc Garoche, Matthieu Martel, Célia Picard
2025	J	`jnl`	Set-based value operators for non-stationary and uncertain Markov decision processes. Autom. Sarah H. Q. Li, Assalé Adjé, Pierre-Loïc Garoche, Behçet Açikmese
2024	—	`conf`	SCvxPyGen: Autocoding SCvx Algorithm. CDC Danil Berrah, Alexandre Chapoutot, Pierre-Loïc Garoche
2023	—	`conf`	Code-Level Formal Verification of Ellipsoidal Invariant Sets for Linear Parameter-Varying Systems. NFM Elias Khalife, Pierre-Loïc Garoche, Mazen Farhood
2023	J	`jnl`	Equation-Directed Axiomatization of Lustre Semantics to Enable Optimized Code Validation. ACM Trans. Embed. Comput. Syst. Lélio Brun, Christophe Garion, Pierre-Loïc Garoche, Xavier Thirioux
2023	—	`conf`	Towards Proved Formal Specification and Verification of STL Operators as Synchronous Observers. FMAS@iFM Céline Bellanger, Pierre-Loïc Garoche, Matthieu Martel, Célia Picard
2022	J	`jnl`	An Efficient Summation Algorithm for the Accuracy, Convergence and Reproducibility of Parallel Numerical Methods. CoRR Farah Benmouhoub, Pierre-Loïc Garoche, Matthieu Martel
2022	J	`jnl`	Exact Computation of Maximal Invariant Sets for Safe Markov Chains - Lattice Theoretic Approach. IEEE Trans. Autom. Control. Dylan Janak, Pierre-Loïc Garoche, Behçet Açikmese
2022	—	`conf`	Reachability Analysis of Linear Parameter-Varying Systems with Neural Network Controllers. CCTA Arash Sadeghzadeh, Pierre-Loïc Garoche
2022	C	`conf`	Reachability Set Analysis of Closed-Loop Nonlinear Systems with Neural Network Controllers. ACC Arash Sadeghzadeh, Pierre-Loïc Garoche
2022	J	`jnl`	Reducing Collision Risk in Multi-Agent Path Planning: Application to Air traffic Management. CoRR Sarah H. Q. Li, Avi Mittal, Pierre-Loïc Garoche, Behçet Açikmese
2022	J	`jnl`	Set-based value operators for non-stationary Markovian environments. CoRR Sarah H. Q. Li, Assalé Adjé, Pierre-Loïc Garoche, Behçet Açikmese
2022	—	`conf`	Successive Convexification for Optimal Control with Signal Temporal Logic Specifications. HSCC Yuanqi Mao, Behçet Açikmese, Pierre-Loïc Garoche, Alexandre Chapoutot
2021	—	`conf`	An Efficient Summation Algorithm for the Accuracy, Convergence and Reproducibility of Parallel Numerical Methods. VSTTE Farah Benmouhoub, Pierre-Loïc Garoche, Matthieu Martel
2021	J	`jnl`	Bounding fixed points of set-based Bellman operator and Nash equilibria of stochastic games. Autom. Sarah H. Q. Li, Assalé Adjé, Pierre-Loïc Garoche, Behçet Açikmese
2021	C	`conf`	Computing State Invariants Using Point-Wise Integral Quadratic Constraints and the S-procedure. ACC Dany Abou Jaoude, Pierre-Loïc Garoche, Mazen Farhood
2021	J	`jnl`	From Lustre to Simulink: Reverse Compilation for Embedded Systems Applications. ACM Trans. Cyber Phys. Syst. Hamza Bourbouh, Pierre-Loïc Garoche, Christophe Garion, Xavier Thirioux
2021	J	`jnl`	Parabolic set simulation for reachability analysis of linear time-invariant systems with integral quadratic constraint. Eur. J. Control Paul Rousse, Pierre-Loïc Garoche, Didier Henrion
2021	—	`conf`	Parallel Accurate and Reproducible Summation. SAI (1) Farah Benmouhoub, Pierre-Loïc Garoche, Matthieu Martel
2020	—	`conf`	A Continuation Method for computation of H∞ gains of Linear Continuous-Time Periodic Systems. CDC Paul Rousse, John Hauser, Pierre-Loïc Garoche
2020	J	`jnl`	Bounding Fixed Points of Set-Based Bellman Operator and Nash Equilibria of Stochastic Games. CoRR Sarah H. Q. Li, Assalé Adjé, Pierre-Loïc Garoche, Behçet Açikmese
2020	—	`conf`	Bridging the Gap Between Requirements and Simulink Model Analysis. REFSQ Workshops Anastasia Mavridou, Hamza Bourbouh, Pierre-Loïc Garoche, Dimitra Giannakopoulou, Thomas Pressburger, Johann Schumann
2020	J	`jnl`	Fixed Points of the Set-Based Bellman Operator. CoRR Sarah H. Q. Li, Assalé Adjé, Pierre-Loïc Garoche, Behçet Açikmese
2020	A	`conf`	The Ten Lockheed Martin Cyber-Physical Challenges: Formalized, Analyzed, and Explained. RE Anastasia Mavridou, Hamza Bourbouh, Dimitra Giannakopoulou, Thomas Pressburger, Mohammad Hejase, Pierre-Loïc Garoche, Johann Schumann
2020	J	`jnl`	Verification and Validation of Convex Optimization Algorithms for Model Predictive Control. CoRR Raphaël Cohen, Eric Feron, Pierre-Loïc Garoche
2020	J	`jnl`	Verification and Validation of Convex Optimization Algorithms for Model Predictive Control. J. Aerosp. Inf. Syst. Raphael Cohen, Eric Feron, Pierre-Loïc Garoche
2019	—	`conf`	Guaranteed Simulation of Dynamical Systems with Integral Constraints and Application on Delayed Dynamical Systems. CyPhy/WESE Paul Rousse, Julien Alexandre Dit Sandretto, Alexandre Chapoutot, Pierre-Loïc Garoche
2019	—	`conf`	Parabolic Set Simulation for Reachability Analysis of Linear Time Invariant Systems with Integral Quadratic Constraint. ECC Paul Rousse, Pierre-Loïc Garoche, Didier Henrion
2019	J	`jnl`	Parabolic Set Simulation for Reachability Analysis of Linear Time Invariant Systems with Integral Quadratic Constraint. CoRR Paul Rousse, Pierre-Loïc Garoche, Didier Henrion
2019	J	`jnl`	Semidefinite Approximations of Reachable Sets for Discrete-time Polynomial Systems. SIAM J. Control. Optim. Victor Magron, Pierre-Loïc Garoche, Didier Henrion, Xavier Thirioux
2018	—	`conf`	Credible Autocoding of The Ellipsoid Algorithm Solving Second-Order Cone Programs. CDC Raphael Cohen, Eric Feron, Pierre-Loïc Garoche
2018	B	`conf`	Experiments in Verification of Linear Model Predictive Control: Automatic Generation and Formal Verification of an Interior Point Method Algorithm. LPAR Guillaume Davy, Eric Feron, Pierre-Loïc Garoche, Didier Henrion
2018	J	`jnl`	Formal verification of an interior point algorithm instanciation. CoRR Guillaume Davy, Eric Feron, Pierre-Loïc Garoche, Didier Henrion
2018	C	`conf`	Preserving Functional Correctness of Cyber-Physical System Controllers: From Model to Code. FDL Guillaume Davy, Christophe Garion, Pierre-Loïc Garoche, Pierre Roux, Xavier Thirioux
2017	B	`conf`	Automated analysis of Stateflow models. LPAR Hamza Bourbouh, Pierre-Loïc Garoche, Christophe Garion, Arie Gurfinkel, Temesghen Kahsai, Xavier Thirioux
2017	J	`jnl`	Automatic synthesis of k-inductive piecewise quadratic invariants for switched affine control programs. Comput. Lang. Syst. Struct. Assalé Adjé, Pierre-Loïc Garoche
2017	J	`jnl`	Foundations of Intelligent Additive Manufacturing. CoRR Kévin Garanger, Eric Feron, Pierre-Loïc Garoche, Julian J. Rimoli, John D. Berrigan, Martha A. Grover, Kerianne Hobbs
2016	—	`book`	Convex Optimization-based Static Analysis for Control Systems. (Analyse statique de contrôleurs à base d'optimisation convexe). Pierre-Loïc Garoche
2016	—	`conf`	Formal Analysis of Robustness at Model and Code Level. HSCC Timothy E. Wang, Pierre-Loïc Garoche, Pierre Roux, Romain Jobredeaux, Eric Feron
2016	—	`conf`	Hierarchical State Machines as Modular Horn Clauses. HCVS@ETAPS Pierre-Loïc Garoche, Temesghen Kahsai, Xavier Thirioux
2015	J	`jnl`	A Sums-of-Squares Extension of Policy Iterations. CoRR Assalé Adjé, Pierre-Loïc Garoche, Victor Magron
2015	B	`conf`	Automatic Synthesis of Piecewise Linear Quadratic Invariants for Programs. VMCAI Assalé Adjé, Pierre-Loïc Garoche
2015	—	`conf`	Closed loop analysis of control command software. HSCC Pierre Roux, Romain Jobredeaux, Pierre-Loïc Garoche
2015	Misc	`conf`	Compilation of synchronous observers as code contracts. SAC Arnaud Dieumegard, Pierre-Loïc Garoche, Temesghen Kahsai, Alice Taillar, Xavier Thirioux
2015	J	`jnl`	Practical policy iterations - A practical use of policy iterations for static analysis: the quadratic case. Formal Methods Syst. Des. Pierre Roux, Pierre-Loïc Garoche
2015	B	`conf`	Property-based Polynomial Invariant Generation Using Sums-of-Squares Optimization. SAS Assalé Adjé, Pierre-Loïc Garoche, Victor Magron
2015	J	`jnl`	Property-based Polynomial Invariant Generation using Sums-of-Squares Optimization. CoRR Assalé Adjé, Pierre-Loïc Garoche, Victor Magron
2015	B	`conf`	Quadratic Zonotopes - An Extension of Zonotopes to Quadratic Arithmetics. APLAS Assalé Adjé, Pierre-Loïc Garoche, Alexis Werey
2014	J	`jnl`	Automatic Synthesis of Piecewise Linear Quadratic Invariants for Programs. CoRR Assalé Adjé, Pierre-Loïc Garoche
2014	B	`conf`	Computing Quadratic Invariants with Min- and Max-Policy Iterations: A Practical Comparison. FM Pierre Roux, Pierre-Loïc Garoche
2014	J	`jnl`	Credible Autocoding of Convex Optimization Algorithms. CoRR Timothy Wang, Romain Jobredeaux, Marc Pantel, Pierre-Loïc Garoche, Eric Feron, Didier Henrion
2014	J	`jnl`	Quadratic Zonotopes: An extension of Zonotopes to Quadratic Arithmetics. CoRR Assalé Adjé, Pierre-Loïc Garoche, Alexis Werey
2014	—	`conf`	Synthesizing Modular Invariants for Synchronous Code. HCVS Pierre-Loïc Garoche, Arie Gurfinkel, Temesghen Kahsai
2014	—	`conf`	Testing-Based Compiler Validation for Synchronous Languages. NASA Formal Methods Pierre-Loïc Garoche, Falk Howar, Temesghen Kahsai, Xavier Thirioux
2013	C	`conf`	Formal Methods for the Analysis of Critical Control Systems Models: Combining Non-linear and Linear Analyses. FMICS Adrien Champion, Rémi Delmas, Michael Dierkes, Pierre-Loïc Garoche, Romain Jobredeaux, Pierre Roux
2013	J	`jnl`	From Design to Implementation: an Automated, Credible Autocoding Chain for Control Systems. CoRR Timothy Wang, Romain Jobredeaux, Heber Herencia-Zapana, Pierre-Loïc Garoche, Arnaud Dieumegard, Eric Feron, Marc Pantel
2013	—	`conf`	Incremental Invariant Generation Using Logic-Based Automatic Abstract Transformers. NASA Formal Methods Pierre-Loïc Garoche, Temesghen Kahsai, Cesare Tinelli
2013	B	`conf`	Integrating Policy Iterations in Abstract Interpreters. ATVA Pierre Roux, Pierre-Loïc Garoche
2012	—	`conf`	A generic ellipsoid abstract domain for linear time invariant systems. HSCC Pierre Roux, Romain Jobredeaux, Pierre-Loïc Garoche, Eric Feron
2012	—	`conf`	Incremental Verification with Mode Variable Invariants in State Machines. NASA Formal Methods Temesghen Kahsai, Pierre-Loïc Garoche, Cesare Tinelli, Mike Whalen
2012	J	`jnl`	Invariant stream generators using automatic abstract transformers based on a decidable logic CoRR Pierre-Loïc Garoche, Temesghen Kahsai, Cesare Tinelli
2012	—	`conf`	PVS Linear Algebra Libraries for Verification of Control Software Algorithms in C/ACSL. NASA Formal Methods Heber Herencia-Zapana, Romain Jobredeaux, Sam Owre, Pierre-Loïc Garoche, Eric Feron, Gilberto Pérez, Pablo Ascariz
2010	—	`conf`	SMT-AI: an Abstract Interpreter as Oracle for k-induction. TAPAS@SAS Pierre Roux, Remi Delmas, Pierre-Loïc Garoche
2009	J	`jnl`	Essay on Semantics Definition in MDE - An Instrumented Approach for Model Verification. J. Softw. Benoît Combemale, Xavier Crégut, Pierre-Loïc Garoche, Xavier Thirioux
2008	—	`—`	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
2007	—	`conf`	A Property-Driven Approach to Formal Verification of Process Models. ICEIS (Selected Papers) Benoît Combemale, Xavier Crégut, Pierre-Loïc Garoche, Xavier Thirioux, François Vernadat
2007	J	`jnl`	Abstract Interpretation-based Static Safety for Actors. J. Softw. Pierre-Loïc Garoche, Marc Pantel, Xavier Thirioux
2007	—	`conf`	Towards a Formal Verification of Process Model's Properties SIMPLEPDL and TOCL Case Study. ICEIS (3) Benoît Combemale, Pierre-Loïc Garoche, Xavier Crégut, Xavier Thirioux, François Vernadat
2006	A*	`conf`	Accurate Centralization for Applying Model Checking on Networked Applications. ASE Cyrille Artho, Pierre-Loïc Garoche
2006	—	`conf`	Adaptive Geographically Bound Mobile Agents. MSN Kenji Tei, Christian Sommer, Yoshiaki Fukazawa, Shinichi Honiden, Pierre-Loïc Garoche
2006	J	`jnl`	Static Safety for an Actor Dedicated Process Calculus by Abstract Interpretation CoRR Pierre-Loïc Garoche, Marc Pantel, Xavier Thirioux
2006	—	`conf`	Static Safety for an Actor Dedicated Process Calculus by Abstract Interpretation. FMOODS Pierre-Loïc Garoche, Marc Pantel, Xavier Thirioux