Publications
2026 (2)
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}
}
2025 (7)
Automated Fixed-Point Precision Optimization for FPGA Synthesis
Inès Winandy, Arnaud Dion, Florent Manni, Pierre-Loïc Garoche, Dorra Ben Khalifa et al.
IEEE Open J. Circuits Syst., vol. 6, pp. 192–204, 2025 Journal
DOI BibTeX
@article{DBLP:journals/ojcands/WinandyDMGKM25,
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/journals/ojcands/WinandyDMGKM25.bib},
timestamp = {Tue, 05 Aug 2025 22:49:34 +0200},
doi = {10.1109/OJCAS.2025.3580744},
url = {https://doi.org/10.1109/OJCAS.2025.3580744},
year = {2025},
pages = {192--204},
volume = {6},
journal = {IEEE Open J. Circuits Syst.},
title = {Automated Fixed-Point Precision Optimization for FPGA Synthesis},
author = {Inès Winandy and
Arnaud Dion and
Florent Manni and
Pierre-Loïc Garoche and
Dorra Ben Khalifa and
Matthieu Martel}
}
Emergency Trajectory Structure for UAVs
Maëva Ongale-Obeyi, Damien Goubinat, Daniel Delahaye, Pierre-Loïc Garoche
Aerospace, vol. 12(1), 2025 Journal
DOI URL BibTeX
@article{aerospace12010021,
doi = {10.3390/aerospace12010021},
issn = {2226-4310},
url = {https://www.mdpi.com/2226-4310/12/1/21},
article-number = {21},
number = {1},
year = {2025},
volume = {12},
journal = {Aerospace},
title = {Emergency Trajectory Structure for UAVs},
author = {Ongale-Obeyi, Maëva and Goubinat, Damien and Delahaye, Daniel and Garoche, Pierre-Loïc}
}
Formal specification and SMT verification of quantized neural network for autonomous vehicles
Wahiba Bachiri, Yassamine Seladji, Pierre-Loïc Garoche
Sci. Comput. Program., vol. 245, pp. 103316, 2025 Journal
DOI BibTeX
@article{DBLP:journals/scp/BachiriSG25,
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/journals/scp/BachiriSG25.bib},
timestamp = {Fri, 09 May 2025 20:27:47 +0200},
doi = {10.1016/J.SCICO.2025.103316},
url = {https://doi.org/10.1016/j.scico.2025.103316},
year = {2025},
pages = {103316},
volume = {245},
journal = {Sci. Comput. Program.},
title = {Formal specification and SMT verification of quantized neural network
for autonomous vehicles},
author = {Wahiba Bachiri and
Yassamine Seladji and
Pierre-Loïc Garoche}
}
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., vol. 245, pp. 103315, 2025 Journal
DOI BibTeX
@article{DBLP:journals/scp/BellangerGMP25,
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/journals/scp/BellangerGMP25.bib},
timestamp = {Wed, 07 May 2025 11:25:50 +0200},
doi = {10.1016/J.SCICO.2025.103315},
url = {https://doi.org/10.1016/j.scico.2025.103315},
year = {2025},
pages = {103315},
volume = {245},
journal = {Sci. Comput. Program.},
title = {Formally proved specification of non-nested STL formulas as synchronous
observers},
author = {Céline Bellanger and
Pierre-Loïc Garoche and
Matthieu Martel and
Célia Picard}
}
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., vol. 171, pp. 111970, 2025 Journal
DOI BibTeX
@article{DBLP:journals/automatica/LiAGA25,
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/journals/automatica/LiAGA25.bib},
timestamp = {Mon, 09 Dec 2024 22:47:49 +0100},
doi = {10.1016/J.AUTOMATICA.2024.111970},
url = {https://doi.org/10.1016/j.automatica.2024.111970},
year = {2025},
pages = {111970},
volume = {171},
journal = {Autom.},
title = {Set-based value operators for non-stationary and uncertain Markov
decision processes},
author = {Sarah H. Q. Li and
Assalé Adjé and
Pierre-Loïc Garoche and
Behçet Açikmese}
}
Formally Proving Invariant Systemic Properties of Control Programs Using Ghost Code and Integral Quadratic Constraints
Elias Khalife, Pierre-Loïc Garoche, Mazen Farhood
NASA Formal Methods - 17th International Symposium, NFM 2025, Williamsburg, VA, USA, June 11-13, 2025, Proceedings, vol. 15682, pp. 180–200 Conference
DOI BibTeX
@inproceedings{DBLP:conf/nfm/KhalifeGF25,
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/conf/nfm/KhalifeGF25.bib},
timestamp = {Mon, 16 Jun 2025 17:30:19 +0200},
doi = {10.1007/978-3-031-93706-4_11},
url = {https://doi.org/10.1007/978-3-031-93706-4_11},
year = {2025},
publisher = {Springer},
pages = {180--200},
volume = {15682},
series = {Lecture Notes in Computer Science},
booktitle = {NASA Formal Methods - 17th International Symposium, NFM 2025,
Williamsburg, VA, USA, June 11-13, 2025, Proceedings},
title = {Formally Proving Invariant Systemic Properties of Control Programs
Using Ghost Code and Integral Quadratic Constraints},
editor = {Aaron Dutle and
Laura R. Humphrey and
Laura Titolo},
author = {Elias Khalife and
Pierre-Loïc Garoche and
Mazen Farhood}
}
PYXIS: A higly predictable toolchain for FPGA circuit production of advanced GNC algorithm
Inès Winandy, Arnaud Dion, Pierre-Loïc Garoche, Florent Manni
SMC-IT/SCC 2025 Conference
URL PDF BibTeX
@inproceedings{winandy:hal-05080319,
hal_version = {v1},
hal_id = {hal-05080319},
month = {July},
year = {2025},
address = {Los Angeles, United States},
booktitle = {SMC-IT/SCC 2025},
url = {https://hal.science/hal-05080319},
author = {Winandy, Inès and Dion, Arnaud and Garoche, Pierre-Loïc and Manni, Florent},
title = {PYXIS: A higly predictable toolchain for FPGA circuit production of advanced GNC algorithm}
}
2024 (4)
A Reactive System-specific Compilation Chain from Synchronous Dataflow Models to FPGA Netlist
Inès Winandy, Arnaud Dion, Pierre-Loı̈c Garoche, Florent Manni
2024 IEEE 10th International Conference on Space Mission Challenges for Information Technology (SMC-IT), pp. 11–21 Conference
DOI BibTeX
@inproceedings{winandy2024reactive,
doi = {10.1109/SMC-IT61443.2024.00009},
organization = {IEEE},
year = {2024},
pages = {11--21},
booktitle = {2024 IEEE 10th International Conference on Space Mission Challenges for Information Technology (SMC-IT)},
author = {Winandy, Inès and Dion, Arnaud and Garoche, Pierre-Loı̈c and Manni, Florent},
title = {A Reactive System-specific Compilation Chain from Synchronous Dataflow Models to FPGA Netlist}
}
Formal Verification of Quantized Neural Network
Wahiba Bachiri, Yassamine Seladji, Pierre-Loı̈c Garoche
2024 International Conference of the African Federation of Operational Research Societies (AFROS), pp. https–ieeexplore Conference
BibTeX
@inproceedings{bachiri2024formal,
organization = {IEEE},
year = {2024},
pages = {https--ieeexplore},
booktitle = {2024 International Conference of the African Federation of Operational Research Societies (AFROS)},
author = {Bachiri, Wahiba and Seladji, Yassamine and Garoche, Pierre-Loı̈c},
title = {Formal Verification of Quantized Neural Network}
}
SCvxPyGen: Autocoding SCvx Algorithm
Danil Berrah, Alexandre Chapoutot, Pierre-Loïc Garoche
63rd IEEE Conference on Decision and Control, CDC 2024, Milan, Italy, December 16-19, 2024, pp. 5086–5093 Conference
DOI BibTeX
@inproceedings{DBLP:conf/cdc/BerrahCG24,
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/conf/cdc/BerrahCG24.bib},
timestamp = {Tue, 05 Aug 2025 22:38:34 +0200},
doi = {10.1109/CDC56724.2024.10886875},
url = {https://doi.org/10.1109/CDC56724.2024.10886875},
year = {2024},
publisher = {IEEE},
pages = {5086--5093},
booktitle = {63rd IEEE Conference on Decision and Control, CDC 2024, Milan,
Italy, December 16-19, 2024},
title = {SCvxPyGen: Autocoding SCvx Algorithm},
author = {Danil Berrah and
Alexandre Chapoutot and
Pierre-Loïc Garoche}
}
Verification & validation of optimisation-based control systems: methods and outcomes of VV4RTOS
Pedro Lourenço, Hugo Costa, João Branco, Pierre-Loïc Garoche, Arash Sadeghzadeh et al.
ESA GNC 2023, 2024 Conference
DOI BibTeX
@inproceedings{esagnc23,
doi = {10.5270/esa-gnc-icatt-2023-155},
year = {2024},
booktitle = {ESA GNC 2023},
title = {Verification & validation of optimisation-based control systems: methods and outcomes of VV4RTOS},
author = {Pedro Lourenço and Hugo Costa and João Branco and Pierre-Loïc Garoche and Arash Sadeghzadeh and Jonathan Frey and Gianluca Frison and Anthea Comellini and Massimo Barbero and Valentin Preda}
}
2023 (5)
Autoencoder Neural Networks for LPV Embedding of Nonlinear Systems
Arash Sadeghzadeh, Pierre-Loïc Garoche
IFAC-PapersOnLine, vol. 56(2), pp. 9062-9067, 2023 Journal
DOI URL BibTeX
@article{SADEGHZADEH20239062,
author = {Arash Sadeghzadeh and Pierre-Loïc Garoche},
url = {https://www.sciencedirect.com/science/article/pii/S2405896323004846},
doi = {https://doi.org/10.1016/j.ifacol.2023.10.137},
issn = {2405-8963},
note = {22nd IFAC World Congress},
year = {2023},
pages = {9062-9067},
number = {2},
volume = {56},
journal = {IFAC-PapersOnLine},
title = {Autoencoder Neural Networks for LPV Embedding of Nonlinear Systems}
}
Computation of invariant sets for discrete-time uncertain systems
Elias Khalife, Dany Abou Jaoude, Mazen Farhood, Pierre-Loic Garoche
International Journal of Robust and Nonlinear Control, vol. 33(14), pp. 8452-8474, 2023 Journal
DOI URL BibTeX
@article{https://doi.org/10.1002/rnc.6834,
year = {2023},
eprint = {https://onlinelibrary.wiley.com/doi/pdf/10.1002/rnc.6834},
url = {https://onlinelibrary.wiley.com/doi/abs/10.1002/rnc.6834},
doi = {https://doi.org/10.1002/rnc.6834},
pages = {8452-8474},
number = {14},
volume = {33},
journal = {International Journal of Robust and Nonlinear Control},
title = {Computation of invariant sets for discrete-time uncertain systems},
author = {Khalife, Elias and Abou Jaoude, Dany and Farhood, Mazen and Garoche, Pierre-Loic}
}
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., vol. 22(5s), pp. 151:1–151:24, 2023 Journal
DOI BibTeX
@article{DBLP:journals/tecs/BrunGGT23,
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/journals/tecs/BrunGGT23.bib},
timestamp = {Sat, 28 Oct 2023 13:59:33 +0200},
doi = {10.1145/3609393},
url = {https://doi.org/10.1145/3609393},
year = {2023},
pages = {151:1--151:24},
number = {5s},
volume = {22},
journal = {ACM Trans. Embed. Comput. Syst.},
title = {Equation-Directed Axiomatization of Lustre Semantics to Enable Optimized
Code Validation},
author = {Lélio Brun and
Christophe Garion and
Pierre-Loïc Garoche and
Xavier Thirioux}
}
Code-Level Formal Verification of Ellipsoidal Invariant Sets for Linear Parameter-Varying Systems
Elias Khalife, Pierre-Loïc Garoche, Mazen Farhood
NASA Formal Methods - 15th International Symposium, NFM 2023, Houston, TX, USA, May 16-18, 2023, Proceedings, vol. 13903, pp. 157–173 Conference
DOI BibTeX
@inproceedings{DBLP:conf/nfm/KhalifeGF23,
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/conf/nfm/KhalifeGF23.bib},
timestamp = {Mon, 26 Jun 2023 16:11:22 +0200},
doi = {10.1007/978-3-031-33170-1_10},
url = {https://doi.org/10.1007/978-3-031-33170-1_10},
year = {2023},
publisher = {Springer},
pages = {157--173},
volume = {13903},
series = {Lecture Notes in Computer Science},
booktitle = {NASA Formal Methods - 15th International Symposium, NFM 2023,
Houston, TX, USA, May 16-18, 2023, Proceedings},
title = {Code-Level Formal Verification of Ellipsoidal Invariant Sets for Linear
Parameter-Varying Systems},
editor = {Kristin Yvonne Rozier and
Swarat Chaudhuri},
author = {Elias Khalife and
Pierre-Loïc Garoche and
Mazen Farhood}
}
Towards Proved Formal Specification and Verification of STL Operators as Synchronous Observers
Céline Bellanger, Pierre-Loïc Garoche, Matthieu Martel, Célia Picard
Proceedings Fifth International Workshop on Formal Methods for Autonomous Systems, FMAS@iFM 2023, Leiden, The Netherlands, 15th and 16th of November 2023, vol. 395, pp. 188–204 Conference
DOI BibTeX
@inproceedings{DBLP:journals/corr/abs-2311-09788,
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/journals/corr/abs-2311-09788.bib},
timestamp = {Fri, 22 Dec 2023 16:43:30 +0100},
doi = {10.4204/EPTCS.395.14},
url = {https://doi.org/10.4204/EPTCS.395.14},
year = {2023},
pages = {188--204},
volume = {395},
series = {EPTCS},
booktitle = {Proceedings Fifth International Workshop on Formal Methods for Autonomous
Systems, FMAS@iFM 2023, Leiden, The Netherlands, 15th and 16th of
November 2023},
title = {Towards Proved Formal Specification and Verification of STL Operators
as Synchronous Observers},
editor = {Marie Farrell and
Matt Luckcuck and
Mario Gleirscher and
Maike Schwammberger},
author = {Céline Bellanger and
Pierre-Loïc Garoche and
Matthieu Martel and
Célia Picard}
}
2022 (6)
Exact Computation of Maximal Invariant Sets for Safe Markov Chains—Lattice Theoretic Approach
Dylan Janak, Pierre-Loïc Garoche, Behçet Açikmese
IEEE Transactions on Automatic Control, 2022 Journal
BibTeX
@article{TAC22,
optannote = {},
optnote = {accepted, to appear},
optmonth = {},
optpages = {},
optnumber = {},
optvolume = {},
optkey = {},
year = {2022},
journal = {IEEE Transactions on Automatic Control},
title = {Exact Computation of Maximal Invariant Sets for Safe Markov Chains—Lattice Theoretic Approach},
author = {Dylan Janak and Pierre-Loïc Garoche and Behçet Açikmese}
}
Reducing collision risk in multi-agent path planning: Application to air traffic management
Sarah HQ Li, Avi Mittal, Pierre-Loı̈c Garoche, others
arXiv preprint arXiv:2212.04122, 2022 Journal
BibTeX
@article{li2022reducing,
year = {2022},
journal = {arXiv preprint arXiv:2212.04122},
author = {Li, Sarah HQ and Mittal, Avi and Garoche, Pierre-Loı̈c and others},
title = {Reducing collision risk in multi-agent path planning: Application to air traffic management}
}
Reachability Analysis of Linear Parameter-Varying Systems with Neural Network Controllers
Arash Sadeghzadeh, Pierre-Loïc Garoche
Conference on Control Technology and Applications, CCTA 2022, Trieste, Italy, August 22-25, 2022 Conference
BibTeX
@inproceedings{CCTA22,
year = {2022},
publisher = {IEEE},
booktitle = {Conference on Control Technology and Applications, CCTA 2022, Trieste, Italy, August 22-25,
2022},
title = {Reachability Analysis of Linear Parameter-Varying Systems with Neural Network Controllers},
author = {Arash Sadeghzadeh and
Pierre-Loïc Garoche}
}
Reachability Set Analysis of Closed-Loop Nonlinear Systems with Neural Network Controllers
Arash Sadeghzadeh, Pierre-Loïc Garoche
American Control Conference, ACC 2022, Atlanta, GA, USA, June 8-10, 2022, pp. 2289–2294 Conference
DOI BibTeX
@inproceedings{DBLP:conf/amcc/SadeghzadehG22,
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/conf/amcc/SadeghzadehG22.bib},
timestamp = {Mon, 12 Sep 2022 17:48:03 +0200},
doi = {10.23919/ACC53348.2022.9867572},
url = {https://doi.org/10.23919/ACC53348.2022.9867572},
year = {2022},
publisher = {IEEE},
pages = {2289--2294},
booktitle = {American Control Conference, ACC 2022, Atlanta, GA, USA, June 8-10,
2022},
title = {Reachability Set Analysis of Closed-Loop Nonlinear Systems with Neural
Network Controllers},
author = {Arash Sadeghzadeh and
Pierre-Loïc Garoche}
}
Successive Convexification for Optimal Control with Signal Temporal Logic Specifications
Yuanqi Mao, Behçet Açikmese, Pierre-Loïc Garoche, Alexandre Chapoutot
HSCC ’22: 25th ACM International Conference on Hybrid Systems: Computation and Control, Milan, Italy, May 4 - 6, 2022, pp. 9:1–9:7 Conference
DOI BibTeX
@inproceedings{DBLP:conf/hybrid/MaoAGC22,
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/conf/hybrid/MaoAGC22.bib},
timestamp = {Thu, 07 Jul 2022 07:10:17 +0200},
doi = {10.1145/3501710.3519518},
url = {https://doi.org/10.1145/3501710.3519518},
year = {2022},
publisher = {ACM},
pages = {9:1--9:7},
booktitle = {HSCC '22: 25th ACM International Conference on Hybrid Systems:
Computation and Control, Milan, Italy, May 4 - 6, 2022},
title = {Successive Convexification for Optimal Control with Signal Temporal
Logic Specifications},
editor = {Ezio Bartocci and
Sylvie Putot},
author = {Yuanqi Mao and
Behçet Açikmese and
Pierre-Loïc Garoche and
Alexandre Chapoutot}
}
Set-based value operators for non-stationary Markovian environments
Sarah H. Q. Li, Assalé Adjé, Pierre-Loïc Garoche, Behçet Açıkmeşe
2022 Preprint
DOI URL BibTeX
@misc{https://doi.org/10.48550/arxiv.2207.07271,
copyright = {arXiv.org perpetual, non-exclusive license},
year = {2022},
publisher = {arXiv},
title = {Set-based value operators for non-stationary Markovian environments},
author = {Li, Sarah H. Q. and Adjé, Assalé and Garoche, Pierre-Loïc and Açıkmeşe, Behçet},
url = {https://arxiv.org/abs/2207.07271},
doi = {10.48550/ARXIV.2207.07271}
}
2021 (7)
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., vol. 130, pp. 109685, 2021 Journal
DOI BibTeX
@article{DBLP:journals/automatica/LiAGA21,
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/journals/automatica/LiAGA21.bib},
timestamp = {Tue, 15 Jun 2021 16:47:59 +0200},
doi = {10.1016/j.automatica.2021.109685},
url = {https://doi.org/10.1016/j.automatica.2021.109685},
year = {2021},
pages = {109685},
volume = {130},
journal = {Autom.},
title = {Bounding fixed points of set-based Bellman operator and Nash equilibria
of stochastic games},
author = {Sarah H. Q. Li and
Assalé Adjé and
Pierre-Loïc Garoche and
Behçet Açikmese}
}
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., vol. 5(3), pp. 31:1–31:20, 2021 Journal
DOI BibTeX
@article{DBLP:journals/tcps/BourbouhGGT21,
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/journals/tcps/BourbouhGGT21.bib},
timestamp = {Wed, 18 Aug 2021 08:47:20 +0200},
doi = {10.1145/3461668},
url = {https://doi.org/10.1145/3461668},
year = {2021},
pages = {31:1--31:20},
number = {3},
volume = {5},
journal = {ACM Trans. Cyber Phys. Syst.},
title = {From Lustre to Simulink: Reverse Compilation for Embedded Systems
Applications},
author = {Hamza Bourbouh and
Pierre-Loïc Garoche and
Christophe Garion and
Xavier Thirioux}
}
Parabolic set simulation for reachability analysis of linear time-invariant systems with integral quadratic constraint
Paul Rousse, Pierre-Loïc Garoche, Didier Henrion
Eur. J. Control, vol. 58, pp. 152–167, 2021 Journal
DOI BibTeX
@article{DBLP:journals/ejcon/RousseGH21,
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/journals/ejcon/RousseGH21.bib},
timestamp = {Wed, 24 Feb 2021 15:26:48 +0100},
doi = {10.1016/j.ejcon.2020.08.002},
url = {https://doi.org/10.1016/j.ejcon.2020.08.002},
year = {2021},
pages = {152--167},
volume = {58},
journal = {Eur. J. Control},
title = {Parabolic set simulation for reachability analysis of linear time-invariant
systems with integral quadratic constraint},
author = {Paul Rousse and
Pierre-Loïc Garoche and
Didier Henrion}
}
An Efficient Summation Algorithm for the Accuracy, Convergence and Reproducibility of Parallel Numerical Methods
Farah Benmouhoub, Pierre-Loic Garoche, Matthieu Martel
Software Verification, pp. 165–181, 2021 Conference
BibTeX
@inproceedings{10.1007/978-3-030-95561-8_10,
isbn = {978-3-030-95561-8},
pages = {165--181},
address = {Cham},
publisher = {Springer International Publishing},
year = {2021},
booktitle = {Software Verification},
title = {An Efficient Summation Algorithm for the Accuracy, Convergence and Reproducibility of Parallel Numerical Methods},
editor = {Bloem, Roderick
and Dimitrova, Rayna
and Fan, Chuchu
and Sharygina, Natasha},
author = {Benmouhoub, Farah
and Garoche, Pierre-Loic
and Martel, Matthieu}
}
Computing State Invariants Using Point-Wise Integral Quadratic Constraints and the S-procedure
Dany Abou Jaoude, Pierre-Loïc Garoche, Mazen Farhood
2021 American Control Conference, ACC 2021, New Orleans, LA, USA, May 25-28, 2021, pp. 2394–2399 Conference
DOI BibTeX
@inproceedings{DBLP:conf/amcc/JaoudeGF21,
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/conf/amcc/JaoudeGF21.bib},
timestamp = {Fri, 30 Jul 2021 11:11:53 +0200},
doi = {10.23919/ACC50511.2021.9483175},
url = {https://doi.org/10.23919/ACC50511.2021.9483175},
year = {2021},
publisher = {IEEE},
pages = {2394--2399},
booktitle = {2021 American Control Conference, ACC 2021, New Orleans, LA, USA,
May 25-28, 2021},
title = {Computing State Invariants Using Point-Wise Integral Quadratic Constraints
and the S-procedure},
author = {Dany Abou Jaoude and
Pierre-Loïc Garoche and
Mazen Farhood}
}
Parallel Accurate and Reproducible Summation
Farah Benmouhoub, Pierre-Loic Garoche, Matthieu Martel
Intelligent Computing, pp. 363–382, 2021 Conference
BibTeX
@inproceedings{10.1007/978-3-030-80119-9_21,
isbn = {978-3-030-80119-9},
pages = {363--382},
address = {Cham},
publisher = {Springer International Publishing},
year = {2021},
booktitle = {Intelligent Computing},
title = {Parallel Accurate and Reproducible Summation},
editor = {Arai, Kohei},
author = {Benmouhoub, Farah
and Garoche, Pierre-Loic
and Martel, Matthieu}
}
Probabilistic swarms guidance within the Gama-platform
Zahia Matta, Robin Barbier, Zakaria Ezzahed, Quentin Vaquier, Pierre-Loïc Garoche
1st conference GAMA Days 2021 Conference
URL BibTeX
@inproceedings{matta:hal-03521268,
hal_version = {v1},
hal_id = {hal-03521268},
month = {June},
year = {2021},
editor = {Frédéric Amblard and Kevin Chapuis and Alexis Drogoul and Benoit Gaudou and Dominique Longin and Nicolas Verstaevel},
organization = {Frédéric Amblard and Kevin Chapuis and Alexis Drogoul and Benoit Gaudou and Dominique Longin and Nicolas Verstaevel},
address = {Toulouse (Online), France},
booktitle = {1st conference GAMA Days 2021},
url = {https://ut3-toulouseinp.hal.science/hal-03521268},
author = {Matta, Zahia and Barbier, Robin and Ezzahed, Zakaria and Vaquier, Quentin and Garoche, Pierre-Loïc},
title = {Probabilistic swarms guidance within the Gama-platform}
}
2020 (10)
Verification and Validation of Convex Optimization Algorithms for Model Predictive Control
Raphael Cohen, Eric Feron, Pierre-Loïc Garoche
Journal of Aerospace Information Systems, vol. 17(5), pp. 257-270, 2020 Journal
DOI URL BibTeX
@article{doi:10.2514/1.I010686,
url = { https://arxiv.org/pdf/2005.12588},
metrics = {impact factor: 2.30},
doi = {10.2514/1.I010686},
month = {3},
year = {2020},
pages = {257-270},
number = {5},
volume = {17},
journal = {Journal of Aerospace Information Systems},
title = {Verification and Validation of Convex Optimization Algorithms for Model Predictive Control},
author = {Cohen, Raphael and Feron, Eric and Garoche, Pierre-Loïc}
}
A Continuation Method for computation of H(ınfty) gains of Linear Continuous-Time Periodic Systems
Paul Rousse, John Hauser, Pierre-Loïc Garoche
59th IEEE Conference on Decision and Control, CDC 2020, Jeju Island, South Korea, December 14-18, 2020, pp. 4653–4658 Conference
DOI BibTeX
@inproceedings{DBLP:conf/cdc/RousseHG20,
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/conf/cdc/RousseHG20.bib},
timestamp = {Tue, 19 Jan 2021 12:30:29 +0100},
doi = {10.1109/CDC42340.2020.9304427},
url = {https://doi.org/10.1109/CDC42340.2020.9304427},
year = {2020},
publisher = {IEEE},
pages = {4653--4658},
booktitle = {59th IEEE Conference on Decision and Control, CDC 2020, Jeju Island,
South Korea, December 14-18, 2020},
title = {A Continuation Method for computation of H\(ınfty\) gains of Linear
Continuous-Time Periodic Systems},
author = {Paul Rousse and
John Hauser and
Pierre-Loïc Garoche}
}
Bridging the Gap Between Requirements and Simulink Model Analysis
Anastasia Mavridou, Hamza Bourbouh, Pierre-Loïc Garoche, Dimitra Giannakopoulou, Thomas Pressburger et al.
Joint Proceedings of REFSQ-2020 Workshops, Doctoral Symposium, Live Studies Track, and Poster Track co-located with the 26th International Conference on Requirements Engineering: Foundation for Software Quality (REFSQ 2020), Pisa, Italy, March 24, 2020, vol. 2584 Conference
URL BibTeX
@inproceedings{DBLP:conf/refsq/MavridouBGGPS20,
metric = {Best Poster},
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/conf/refsq/MavridouBGGPS20.bib},
timestamp = {Tue, 31 Mar 2020 18:05:18 +0200},
url = {http://ceur-ws.org/Vol-2584/PT-paper9.pdf},
year = {2020},
publisher = {CEUR-WS.org},
volume = {2584},
month = {3},
series = {CEUR Workshop Proceedings},
booktitle = {Joint Proceedings of REFSQ-2020 Workshops, Doctoral Symposium, Live
Studies Track, and Poster Track co-located with the 26th International
Conference on Requirements Engineering: Foundation for Software Quality
(REFSQ 2020), Pisa, Italy, March 24, 2020},
title = {Bridging the Gap Between Requirements and Simulink Model Analysis},
editor = {Mehrdad Sabetzadeh and
Andreas Vogelsang and
Sallam Abualhaija and
Markus Borg and
Fabiano Dalpiaz and
Maya Daneva and
Nelly Condori-Fernández and
Xavier Franch and
Davide Fucci and
Vincenzo Gervasi and
Eduard C. Groen and
Renata S. S. Guizzardi and
Andrea Herrmann and
Jennifer Horkoff and
Luisa Mich and
Anna Perini and
Angelo Susi},
author = {Anastasia Mavridou and
Hamza Bourbouh and
Pierre-Loïc Garoche and
Dimitra Giannakopoulou and
Thomas Pressburger and
Johann Schumann}
}
CoCoSim, a code generation framework for control/command applications An overview of CoCoSim for multi-periodic discrete Simulink models
Hamza Bourbouh, Pierre-Loïc Garoche, Thomas Loquen, Éric Noulard, Claire Pagetti
10th European Congress on Embedded Real Time Software and Systems (ERTS 2020) Conference
URL PDF BibTeX
@inproceedings{bourbouh:hal-02441334,
hal_version = {v1},
hal_id = {hal-02441334},
month = {1},
year = {2020},
address = {Toulouse, France},
booktitle = {10th European Congress on Embedded Real Time Software and Systems (ERTS 2020)},
url = {https://hal.archives-ouvertes.fr/hal-02441334},
author = {Bourbouh, Hamza and Garoche, Pierre-Loïc and Loquen, Thomas and Noulard, Éric and Pagetti, Claire},
title = {CoCoSim, a code generation framework for control/command applications An overview of CoCoSim for multi-periodic discrete Simulink models}
}
CoCoSim, a code generation framework for control/command applications An overview of CoCoSim for multi-periodic discrete Simulink models
Hamza Bourbouh, Pierre-Loïc Garoche, Thomas Loquen, Éric Noulard, Claire Pagetti
10th European Congress on Embedded Real Time Software and Systems (ERTS 2020) Conference
URL PDF BibTeX
@inproceedings{bourbouh:hal-02441334,
hal_version = {v1},
hal_id = {hal-02441334},
month = {January},
year = {2020},
address = {Toulouse, France},
booktitle = {10th European Congress on Embedded Real Time Software and Systems (ERTS 2020)},
url = {https://hal.archives-ouvertes.fr/hal-02441334},
author = {Bourbouh, Hamza and Garoche, Pierre-Loïc and Loquen, Thomas and Noulard, Éric and Pagetti, Claire},
title = {CoCoSim, a code generation framework for control/command applications An overview of CoCoSim for multi-periodic discrete Simulink models}
}
CoCoSim: an automated analysis framework for Simulink/Stateflow
Hamza Bourbouh, Guillaume Brat, Pierre-Loïc Garoche
Model Based Space Systems and Software Engineering-European Space Agency Workshop (MBSE 2020) Conference
URL BibTeX
@inproceedings{mbse20,
url = {https://indico.esa.int/event/329/contributions/5542/attachments/3898/5506/1640_-_Abstract_-_CoCoSim_an_automated_analysis_framework_for_SimulinkStateflow.pdf},
year = {2020},
booktitle = {Model Based Space Systems and Software Engineering-European Space Agency Workshop (MBSE 2020)},
title = {CoCoSim: an automated analysis framework for Simulink/Stateflow},
author = {Bourbouh, Hamza and Brat, Guillaume and Garoche, Pierre-Loïc}
}
The Ten Lockheed Martin Cyber-Physical Challenges: Formalized, Analyzed, and Explained
Anastasia Mavridou, Hamza Bourbouh, Dimitra Giannakopoulou, Thomas Pressburger, Mohammad Hejase et al.
Proceedings of the 28th IEEE International Requirements Engineering Conference (RE 2020), Industrial Innovation track, Zurich, Switzerland, Augsut 31, 2020, pp. 300-310 Conference
BibTeX
@inproceedings{re20,
metrics = {rank A, acceptance rate 52%},
year = {2020},
pages = {300-310},
month = {8},
booktitle = {Proceedings of the 28th IEEE International Requirements Engineering Conference
(RE 2020), Industrial Innovation track, Zurich, Switzerland, Augsut 31, 2020},
title = {The Ten Lockheed Martin Cyber-Physical Challenges: Formalized, Analyzed, and Explained},
author = {Anastasia Mavridou and
Hamza Bourbouh and
Dimitra Giannakopoulou and
Thomas Pressburger and
Mohammad Hejase and
Pierre-Loïc Garoche and
Johann Schumann}
}
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çıkmeşe
2020 Preprint
BibTeX
@misc{li2020bounding,
primaryclass = {cs.GT},
archiveprefix = {arXiv},
eprint = {2001.07889},
year = {2020},
author = {Sarah H. Q. Li and Assalé and Adjé and Pierre-Loïc Garoche and Behçet Açıkmeşe},
title = {Bounding Fixed Points of Set-Based Bellman Operator and Nash Equilibria of Stochastic Games}
}
Fixed Points of the Set-Based Bellman Operator
Sarah H. Q. Li, Assalé Adjé, Pierre-Loïc Garoche, Behçet Açıkmeşe
2020 Preprint
BibTeX
@misc{li2020fixed,
primaryclass = {math.OC},
archiveprefix = {arXiv},
eprint = {2001.04535},
year = {2020},
author = {Sarah H. Q. Li and Assalé Adjé and Pierre-Loïc Garoche and Behçet Açıkmeşe},
title = {Fixed Points of the Set-Based Bellman Operator}
}
Towards a Set-based Signal Temporal Logic
Julien Alexandre Dit Sandretto, Alexandre Chapoutot, Pierre-Loïc Garoche
working paper or preprint, 2020 Preprint
URL PDF BibTeX
@unpublished{alexandreditsandretto:hal-03084701,
hal_version = {v1},
hal_id = {hal-03084701},
month = {December},
year = {2020},
note = {working paper or preprint},
url = {https://hal-ensta-paris.archives-ouvertes.fr//hal-03084701},
author = {Alexandre Dit Sandretto, Julien and Chapoutot, Alexandre and Garoche, Pierre-Loïc},
title = {Towards a Set-based Signal Temporal Logic}
}
2019 (6)
Semidefinite Approximations of Reachable Sets for Discrete-time Polynomial Systems
Victor Magron, Pierre-Loic Garoche, Didier Henrion, Xavier Thirioux
SIAM J. Control and Optimization, 2019 Journal
DOI BibTeX
@article{sicon19,
metrics = {impact factor: 2.30},
doi = {10.1137/17M1121044},
journal = {SIAM J. Control and Optimization},
year = {2019},
title = {Semidefinite Approximations of Reachable Sets for Discrete-time Polynomial Systems},
author = {Victor Magron and Pierre-Loic Garoche and Didier Henrion and Xavier Thirioux}
}
Formal Verification of Control System Software
Pierre-Loïc Garoche
2019 Book
BibTeX
@book{garoche_pup,
address = {41 William Street, Princeton, New Jersey 08540 USA},
year = {2019},
publisher = {Princeton University Press},
author = {Garoche, Pierre-Loïc},
title = {Formal Verification of Control System Software}
}
Guaranteed Simulation of Dynamical Systems with Integral Constraints & Application on Delayed Dynamical Systems
Paul Rousse, Julien Alexandre Dit Sandretto, Alexandre Chapoutot, Pierre-Loic Garoche
Workshop on Model-Based Design of Cyber Physical Systems (CyPhy’19), 2019 Conference
BibTeX
@inproceedings{cw19,
year = {2019},
booktitle = {Workshop on Model-Based Design of Cyber Physical Systems (CyPhy'19)},
title = {Guaranteed Simulation of Dynamical Systems with Integral Constraints & Application on Delayed Dynamical Systems},
author = {Rousse, Paul and Alexandre Dit Sandretto, Julien and Chapoutot, Alexandre and Garoche, Pierre-Loic}
}
Improving the Numerical Accuracy of Parallel Programs by Data Mapping
Farah Benmouhoub, Matthieu Martel, Pierre-Loïc Garoche
Numerical and Symbolic Abstract Domains, NSAD’19. Porto, Portugal., 2019 Conference
BibTeX
@inproceedings{nsad19,
year = {2019},
booktitle = {Numerical and Symbolic Abstract Domains, NSAD'19. Porto, Portugal.},
title = {Improving the Numerical Accuracy of Parallel Programs by Data Mapping},
author = {Benmouhoub, Farah and Martel, Matthieu and Garoche, Pierre-Loïc}
}
Parabolic Set Simulation for Reachability Analysis of Linear Time Invariant Systems with Integral Quadratic Constraint
Paul Rousse, Pierre-Loïc Garoche, Didier Henrion
European Control Conference ECC’19, Naples, Italy, 2019 Conference
BibTeX
@inproceedings{ecc19,
optannote = {},
optnote = {},
optpublisher = {},
optorganization = {},
optaddress = {},
optmonth = {},
optpages = {},
optseries = {},
optnumber = {},
optvolume = {},
opteditor = {},
year = {2019},
booktitle = {European Control Conference ECC'19, Naples, Italy},
optkey = {},
optcrossref = {},
title = {Parabolic Set
Simulation for Reachability Analysis of Linear Time Invariant
Systems with Integral Quadratic Constraint},
author = {Paul Rousse and Pierre-Loïc Garoche and Didier Henrion}
}
Evaluation of the FRET and CoCoSim tools on the Ten Lockheed Martin Cyber-Physical Challenge Problems
Anastasia Mavridou, Hamza Bourbouh, Pierre-Loïc Garoche, Mohammad Hejase
Technical Report, NASA, 2019 Tech report
PDF BibTeX
@techreport{NASA/TM-2019-220374,
optannote = {},
note = {84 pages},
month = {8},
optaddress = {},
optnumber = {},
opttype = {},
optkey = {},
year = {2019},
institution = {NASA},
title = {Evaluation of the FRET and CoCoSim tools on the Ten Lockheed Martin Cyber-Physical Challenge Problems},
author = {Mavridou, Anastasia and Bourbouh, Hamza and Garoche, Pierre-Loïc and Hejase, Mohammad}
}
2018 (6)
Automatic Generation and Formal Verification of an Interior Point Method Algorithm
Guillaume Davy, Eric Féron, Pierre-Loïc Garoche, Didier Henrion
Numerical Software Verification, NSV’18, part of FLoC’18. Oxford, UK., 2018 Conference
BibTeX
@inproceedings{nsv18,
year = {2018},
booktitle = {Numerical Software Verification, NSV'18, part of FLoC'18. Oxford, UK.},
title = {Automatic Generation and Formal Verification of an Interior Point Method Algorithm},
author = {Davy, Guillaume and Féron, Eric and Garoche, Pierre-Loïc and Henrion, Didier}
}
Credible Autocoding of The Ellipsoid Algorithm Solving Second-Order Cone Programs
Cohen Raphael, Eric Feron, Pierre-Loic Garoche
2018 IEEE Conference on Decision and Control (CDC), Fontainebleau, Miami Beach, FL, USA Conference
BibTeX
@inproceedings{cdc18,
optannote = {},
optnote = {},
optpublisher = {},
optorganization = {},
optaddress = {},
month = {12},
optpages = {},
optseries = {},
optnumber = {},
optvolume = {},
opteditor = {},
year = {2018},
booktitle = {2018 IEEE Conference on Decision
and Control (CDC), Fontainebleau, Miami
Beach, FL, USA},
optkey = {},
optcrossref = {},
title = {Credible Autocoding of The Ellipsoid Algorithm Solving Second-Order Cone Programs},
author = {Cohen Raphael and Feron, Eric and Garoche, Pierre-Loic}
}
Ensuring functional correctness of cyber-physical system controllers: from model to code analyses
Guillaume Davy, Christophe Garion, Pierre-Loic Garoche, Pierre Roux, Xavier Thirioux
Forum on Specification and Design Languages, Special session on Logic and Mathematics Behind Design Automation, FDL’18, TU Munich 10.9-12.9.2018. Conference
BibTeX
@inproceedings{fdl18,
metrics = {Invited paper},
optannote = {},
optnote = {},
optpublisher = {},
optorganization = {},
optaddress = {},
month = {9},
optpages = {},
optseries = {},
optnumber = {},
optvolume = {},
opteditor = {},
year = {2018},
booktitle = {Forum on Specification and Design Languages, Special session on Logic and Mathematics Behind Design Automation, FDL'18, TU Munich 10.9-12.9.2018.},
optkey = {},
optcrossref = {},
title = {Ensuring functional correctness of cyber-physical system controllers: from model to code analyses},
author = {Guillaume Davy and Christophe Garion and Pierre-Loic Garoche and Pierre Roux and Xavier Thirioux}
}
Experiments in Verification of Linear Model Predictive Control: Automatic Generation and Formal Verification of an Interior Point Method Algorithm
Guillaume Davy, Eric Feron, Pierre-Loic Garoche, Didier Henrion
LPAR-22, 22st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Awassa, Ethiopia, November 16-21, 2018 Conference
BibTeX
@inproceedings{lpar18,
year = {2018},
booktitle = {LPAR-22, 22st International Conference on Logic for Programming, Artificial
Intelligence and Reasoning, Awassa, Ethiopia, November 16-21, 2018},
title = {Experiments in Verification of Linear Model Predictive Control: Automatic Generation and Formal Verification of an Interior Point Method Algorithm},
author = {Guillaume Davy and Eric Feron and Pierre-Loic Garoche and Didier Henrion}
}
Formal verification of an interior point algorithm instanciation
Guillaume Davy, Eric Feron, Pierre-Loïc Garoche, Didier Henrion
Technical Report, vol. abs/1801.03833, 2018 Tech report
URL BibTeX
@techreport{DBLP:journals/corr/abs-1801-03833,
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/bib/journals/corr/abs-1801-03833},
timestamp = {Thu, 01 Feb 2018 19:52:26 +0100},
eprint = {1801.03833},
archiveprefix = {arXiv},
url = {http://arxiv.org/abs/1801.03833},
year = {2018},
volume = {abs/1801.03833},
journal = {CoRR},
title = {Formal verification of an interior point algorithm instanciation},
author = {Guillaume Davy and
Eric Feron and
Pierre-Loïc Garoche and
Didier Henrion}
}
Formal verification of an interior point algorithm instanciation
Guillaume Davy, Eric Féron, Pierre-Loïc Garoche, Didier Henrion
Technical Report, 2018 Tech report
URL PDF BibTeX
@techreport{davy:hal-01681134,
hal_version = {v1},
hal_id = {hal-01681134},
month = {January},
year = {2018},
note = {working paper or preprint},
url = {https://hal.archives-ouvertes.fr/hal-01681134},
author = {Davy, Guillaume and Féron, Eric and Garoche, Pierre-Loïc and Henrion, Didier},
title = {Formal verification of an interior point algorithm instanciation}
}
2017 (13)
A Sums-of-Squares Extension of Policy Iterations
Assale Adje, Pierre-Loic Garoche, Victor Magron
Nonlinear Analysis: Hybrid Systems, vol. 25(Supplement C), pp. 60 - 78, 2017 Journal
DOI URL BibTeX
@article{nahs17,
url = {https://hal.archives-ouvertes.fr/hal-01448179},
author = {Adje, Assale and Garoche, Pierre-Loic and Magron, Victor},
year = {2017},
optnote = {(accepted)},
doi = {10.1016/j.nahs.2017.03.001},
issn = {1751-570X},
pages = {60 - 78},
number = {Supplement C},
volume = {25},
journal = {Nonlinear Analysis: Hybrid Systems},
metrics = {impact factor: 3.192},
title = {A Sums-of-Squares Extension of Policy Iterations}
}
Automatic synthesis of k-inductive piecewise quadratic invariants for switched affine control programs
Assalé Adjé, Pierre-Loïc Garoche
Computer Languages, Systems & Structures (COMLAN), vol. 47, pp. 44–61, 2017 Journal
DOI URL BibTeX
@article{Adje2015,
metrics = {impact factor: 0.556},
author = {Assalé Adjé and Pierre-Loïc Garoche},
url = {http://www.sciencedirect.com/science/article/pii/S1477842415000937},
doi = {10.1016/j.cl.2015.12.002},
issn = {1477-8424},
note = {},
year = {2017},
pages = {44--61},
number = {},
volume = {47},
journal = {Computer Languages, Systems & Structures (COMLAN)},
title = {Automatic synthesis of k-inductive piecewise quadratic invariants for switched affine control programs }
}
Automated analysis of Stateflow models
Hamza Bourbouh, Pierre-Loïc Garoche, Christophe Garion, Arie Gurfinkel, Temesghen Kahsai et al.
LPAR-21, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Maun, Botswana, May 7-12, 2017, pp. 144–161 Conference
URL BibTeX
@inproceedings{lpar17,
metrics = {rank A, acceptance rate 44%},
bibsource = {dblp computer science bibliography, http://dblp.org},
biburl = {http://dblp.org/rec/bib/conf/lpar/BourbouhGGGKT17},
timestamp = {Thu, 23 Nov 2017 16:56:11 +0100},
url = {http://www.easychair.org/publications/paper/340361},
optcrossref = {DBLP:conf/lpar/2017},
year = {2017},
pages = {144--161},
booktitle = {LPAR-21, 21st International Conference on Logic for Programming, Artificial
Intelligence and Reasoning, Maun, Botswana, May 7-12, 2017},
title = {Automated analysis of Stateflow models},
author = {Hamza Bourbouh and
Pierre-Loïc Garoche and
Christophe Garion and
Arie Gurfinkel and
Temesghen Kahsai and
Xavier Thirioux}
}
Formal Verification for Embedded Implementation of Convex Optimization Algorithms
Raphael P. Cohen, Guillaume Davy, Eric M. Feron, Pierre-Loic Garoche
IFAC World Congress 2017 Conference
BibTeX
@inproceedings{ifac17,
year = {2017},
booktitle = {IFAC World Congress 2017},
title = {Formal Verification for Embedded Implementation of Convex Optimization Algorithms},
author = {Cohen, Raphael P. and Davy, Guillaume and Feron, Eric M. and Garoche, Pierre-Loic}
}
Validation of Convex Optimization Algorithms and Credible Implementation for Model Predictive Control
Eric M. Feron, Raphael P. Cohen, Guillaume Davy, Pierre-Loic Garoche
AIAA Information Systems-AIAA Infotech @ Aerospace, AIAA SciTech Forum, (AIAA 2017-0562) Conference
DOI BibTeX
@inproceedings{scitech17,
doi = {http://dx.doi.org/10.2514/6.2017-0562},
year = {2017},
booktitle = {AIAA Information Systems-AIAA Infotech @ Aerospace, AIAA SciTech Forum, (AIAA 2017-0562)},
title = {Validation of Convex Optimization Algorithms and Credible Implementation for Model Predictive Control},
author = {Feron, Eric M. and Cohen, Raphael P. and Davy, Guillaume and Garoche, Pierre-Loic}
}
Foundations of Intelligent Additive Manufacturing
Kévin Garanger, Eric Feron, Pierre-Loïc Garoche, Julian J. Rimoli, John D. Berrigan et al.
Technical Report, vol. abs/1705.00960, 2017 Tech report
URL BibTeX
@techreport{DBLP:journals/corr/GarangerFGRBGH17,
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/bib/journals/corr/GarangerFGRBGH17},
timestamp = {Wed, 07 Jun 2017 14:41:19 +0200},
eprint = {1705.00960},
archiveprefix = {arXiv},
url = {http://arxiv.org/abs/1705.00960},
year = {2017},
volume = {abs/1705.00960},
journal = {CoRR},
title = {Foundations of Intelligent Additive Manufacturing},
author = {Kévin Garanger and
Eric Feron and
Pierre-Loïc Garoche and
Julian J. Rimoli and
John D. Berrigan and
Martha Grover and
Kerianne Hobbs}
}
PEA Valencia : Etat d’avancement à T0+3. RT 1/26976
Julien Brunel, Pierre-Loïc Garoche, Pierre Roux
Technical Report, Onera, 2017 Tech report
BibTeX
@techreport{RT1/26976,
optannote = {},
note = {9 pages},
optmonth = {},
optaddress = {},
optnumber = {},
opttype = {},
optkey = {},
year = {2017},
institution = {Onera},
title = {PEA Valencia : Etat d'avancement à T0+3. RT 1/26976},
author = {Brunel, Julien and Garoche, Pierre-Loïc and Roux, Pierre}
}
PEA Valencia : Etat d’avancement à T0+9. RT 1/26977
Julien Brunel, Pierre-Loïc Garoche, Pierre Roux
Technical Report, Onera, 2017 Tech report
BibTeX
@techreport{RT1/26977,
optannote = {},
note = {55 pages},
optmonth = {},
optaddress = {},
optnumber = {},
opttype = {},
optkey = {},
year = {2017},
institution = {Onera},
title = {PEA Valencia : Etat d'avancement à T0+9. RT 1/26977},
author = {Brunel, Julien and Garoche, Pierre-Loïc and Roux, Pierre}
}
Rapport final CAFEIN. RT 3/21071
Pierre-Loïc Garoche, Frank Verdine, Alexandre Chapoutot, Sylvain Conchon, Matthieu Martel et al.
Technical Report, Onera, 2017 Tech report
BibTeX
@techreport{RT3/21071,
optannote = {},
note = {19 pages},
optmonth = {},
optaddress = {},
optnumber = {},
opttype = {},
optkey = {},
year = {2017},
institution = {Onera},
title = {Rapport final CAFEIN. RT 3/21071},
author = {Garoche, Pierre-Loïc and Verdine, Frank and Chapoutot, Alexandre and Conchon, Sylvain and Martel, Matthieu and Dierkes, Michael}
}
Rapport final VORACE. RT 2/26614
Pierre-Loïc Garoche
Technical Report, Onera, 2017 Tech report
BibTeX
@techreport{RT2/26614,
optannote = {},
note = {37 pages},
optmonth = {},
optaddress = {},
optnumber = {},
opttype = {},
optkey = {},
year = {2017},
institution = {Onera},
title = {Rapport final VORACE. RT 2/26614},
author = {Garoche, Pierre-Loïc}
}
Rapport final de l’Etude CNES : Vérification formelle de code généré automatiquement - R S16-BS0004-045 - COMPARAISON SCADE/LUSTRE/SIMULINK. RT 3/26308
Pierre-Loïc Garoche, Xavier Thirioux
Technical Report, Onera, 2017 Tech report
BibTeX
@techreport{RT3/26308,
optannote = {},
note = {21 pages},
optmonth = {},
optaddress = {},
optnumber = {},
opttype = {},
optkey = {},
year = {2017},
institution = {Onera},
title = {Rapport final de l'Etude CNES : Vérification formelle de code généré automatiquement - R S16-BS0004-045 - COMPARAISON SCADE/LUSTRE/SIMULINK. RT 3/26308},
author = {Garoche, Pierre-Loïc and Thirioux, Xavier}
}
Rapport final de l’Etude CNES : Vérification formelle de code généré automatiquement - R S16-BS0004-045. RT 2/26308
Pierre-Loïc Garoche, Xavier Thirioux, Hamza Bourbouh
Technical Report, Onera, 2017 Tech report
BibTeX
@techreport{RT2/26308,
optannote = {},
note = {81 pages},
optmonth = {},
optaddress = {},
optnumber = {},
opttype = {},
optkey = {},
year = {2017},
institution = {Onera},
title = {Rapport final de l'Etude CNES : Vérification formelle de code généré automatiquement - R S16-BS0004-045. RT 2/26308},
author = {Garoche, Pierre-Loïc and Thirioux, Xavier and Bourbouh, Hamza}
}
Semidefinite Approximations of Reachable Sets for Discrete-time Polynomial Systems
Victor Magron, Pierre-Loic Garoche, Didier Henrion, Xavier Thirioux
Technical Report, 2017 Tech report
BibTeX
@techreport{1703:05085,
eprint = {arXiv:1703.05085},
year = {2017},
title = {Semidefinite Approximations of Reachable Sets for Discrete-time Polynomial Systems},
author = {Victor Magron and Pierre-Loic Garoche and Didier Henrion and Xavier Thirioux}
}
2016 (5)
Credible Autocoding of Convex Optimization Algorithms
Timothy Wang, Romain Jobredeaux, Marc Pantel, Pierre-Loïc Garoche, Eric Feron et al.
Springer Optimization and Engineering, 2016 Journal
URL BibTeX
@article{DBLP:journals/opte/WangJPGFH14,
bibsource = {dblp computer science bibliography, http://dblp.org},
biburl = {http://dblp.uni-trier.de/rec/bib/journals/corr/WangJPGFH14},
timestamp = {Tue, 01 Apr 2014 11:56:46 +0200},
url = {http://arxiv.org/abs/1403.1861},
year = {2016},
metrics = {impact factor: 1.233},
journal = {Springer Optimization and Engineering},
title = {Credible Autocoding of Convex Optimization Algorithms},
author = {Timothy Wang and
Romain Jobredeaux and
Marc Pantel and
Garoche, Pierre-Loïc and
Eric Feron and
Didier Henrion}
}
From Design to Implementation: An Automated, Credible Autocoding Chain for Control Systems
Timothy Wang, Romain Jobredeaux, Heber Herencia, Pierre-Loïc Garoche, Arnaud Dieumegard et al.
Advances in Control System Technology for Aerospace Applications, vol. 460, pp. 137-180, 2016 Book chapter
DOI BibTeX
@inbook{bookchap_springer,
language = {English},
pages = {137-180},
author = {Wang, Timothy and Jobredeaux, Romain and Herencia, Heber and Garoche, Pierre-Loïc and Dieumegard, Arnaud and Feron, Éric and Pantel, Marc},
publisher = {Springer Berlin Heidelberg},
title = {From Design to Implementation: An Automated, Credible Autocoding Chain for Control Systems},
doi = {10.1007/978-3-662-47694-9_5},
editor = {Feron, Eric},
series = {Lecture Notes in Control and Information Sciences},
volume = {460},
booktitle = {Advances in Control System Technology for Aerospace Applications},
isbn = {978-3-662-47693-2},
year = {2016}
}
Formal Analysis of Robustness at Model and Code Level
Timothy Wang, Pierre-Loic Garoche, Pierre Roux, Romain Jobredeaux, Eric Feron
19th International Conference on Hybrid Systems: Computation and Control (part of CPS Week), HSCC’16, Vienna, Austria, April 12-14, 2016, pp. 125-134 Conference
BibTeX
@inproceedings{hscc16,
metrics = {acceptance rate 47% },
pages = { 125-134},
year = {2016},
booktitle = {19th International Conference on Hybrid Systems: Computation and Control
(part of CPS Week), HSCC'16, Vienna, Austria, April 12-14, 2016},
title = {Formal Analysis of Robustness at Model and Code Level},
author = {Wang, Timothy and Pierre-Loic Garoche and Pierre Roux and Romain Jobredeaux and Feron, Eric}
}
Hierarchical State Machines as Modular Horn Clauses
Pierre-Loïc Garoche, Temesghen Kahsai, Xavier Thirioux
Proceedings 3rd Workshop on Horn Clauses for Verification and Synthesis, HCVS@ETAPS 2016, Eindhoven, The Netherlands, 3rd April 2016., pp. 15–28 Conference
DOI BibTeX
@inproceedings{DBLP:journals/corr/GarocheKT16,
bibsource = {dblp computer science bibliography, http://dblp.org},
biburl = {http://dblp.uni-trier.de/rec/bib/journals/corr/GarocheKT16},
timestamp = {Wed, 12 Apr 2017 15:09:56 +0200},
doi = {10.4204/EPTCS.219.2},
url = {http://dx.doi.org/10.4204/EPTCS.219.2},
year = {2016},
pages = {15--28},
booktitle = {Proceedings 3rd Workshop on Horn Clauses for Verification and Synthesis,
HCVS@ETAPS 2016, Eindhoven, The Netherlands, 3rd April 2016.},
title = {Hierarchical State Machines as Modular Horn Clauses},
author = {Pierre-Loïc Garoche and
Temesghen Kahsai and
Xavier Thirioux}
}
Convex Optimization-based Static Analysis for Control Systems
Pierre-Loïc Garoche
University of Toulouse, INPT, 2016 PhD thesis
URL BibTeX
@phdthesis{hdr,
optannote = {},
url = {https://tel.archives-ouvertes.fr/tel-01371978},
optnote = {},
month = {september},
optaddress = {},
opttype = {},
optkey = {},
year = {2016},
school = {University of Toulouse, INPT},
title = {Convex Optimization-based Static Analysis for Control Systems},
author = {Garoche, Pierre-Loïc}
}
2015 (10)
Practical Policy Iterations A practical use of policy iterations for static analysis - The quadratic case.
Pierre Roux, Pierre-Loic Garoche
Formal Methods in System Design, vol. 46(2), pp. 163–196, 2015 Journal
DOI BibTeX
@article{fmsd15,
metrics = {impact factor: 0.875},
bibsource = {dblp computer science bibliography, http://dblp.org},
biburl = {http://dblp.uni-trier.de/rec/bib/journals/fmsd/RouxG15},
timestamp = {Tue, 12 May 2015 14:21:44 +0200},
doi = {10.1007/s10703-015-0230-7},
year = {2015},
pages = {163--196},
number = {2},
volume = {46},
journal = {Formal Methods in System Design},
title = {Practical Policy Iterations
A practical use of policy iterations for static analysis - The quadratic case.},
author = {Pierre Roux and Pierre-Loic Garoche}
}
Automatic Synthesis of Piecewise Linear Quadratic Invariants for Programs
Assalé Adjé, Pierre-Loïc Garoche
Verification, Model Checking, and Abstract Interpretation - 16th International Conference, VMCAI 2015, Mumbai, India, January 12-14, 2015. Proceedings, pp. 99–116 Conference
DOI BibTeX
@inproceedings{DBLP:conf/vmcai/AdjeG15,
metrics = {rank B, acceptance rate 45%},
bibsource = {dblp computer science bibliography, http://dblp.org},
biburl = {http://dblp.uni-trier.de/rec/bib/conf/vmcai/AdjeG15},
timestamp = {Fri, 12 Dec 2014 12:30:11 +0100},
doi = {10.1007/978-3-662-46081-8_6},
optcrossref = {DBLP:conf/vmcai/2015},
year = {2015},
pages = {99--116},
booktitle = {Verification, Model Checking, and Abstract Interpretation - 16th International
Conference, VMCAI 2015, Mumbai, India, January 12-14, 2015. Proceedings},
title = {Automatic Synthesis of Piecewise Linear Quadratic Invariants for Programs},
author = {Assalé Adjé and
Garoche, Pierre-Loïc}
}
Closed Loop Analysis of Control Command Software
Pierre Roux, Romain Jobredeaux, Pierre-Loic Garoche
18th International Conference on Hybrid Systems: Computation and Control (part of CPS Week), HSCC’15, Seattle, Washington, USA, April 14-16, 2015, pp. 108–117 Conference
DOI URL BibTeX
@inproceedings{hscc15,
isbn = {978-1-4503-3433-4},
editor = {Antoine Girard and
Sriram Sankaranarayanan},
bibsource = {dblp computer science bibliography, http://dblp.org},
biburl = {http://dblp.uni-trier.de/rec/bib/conf/hybrid/RouxJG15},
timestamp = {Sun, 17 May 2015 09:37:16 +0200},
doi = {10.1145/2728606.2728623},
url = {http://doi.acm.org/10.1145/2728606.2728623},
optcrossref = {DBLP:conf/hybrid/2015},
pages = {108--117},
year = {2015},
metrics = {acceptance rate 34% },
booktitle = {18th International Conference on Hybrid Systems: Computation and Control (part of CPS Week), HSCC'15, Seattle, Washington, USA, April 14-16, 2015},
title = {Closed Loop Analysis of Control Command Software},
author = {Pierre Roux and Romain Jobredeaux and Pierre-Loic Garoche}
}
Compilation Of Synchronous Observers As Code Contracts
Arnaud Dieumegard, Pierre-Loic Garoche, Temesghen Kahsai, Alice Tailliar, Xavier Thirioux
30th ACM/SIGAPP Symposium on Applied Computing, SAC 2015, Salamanca, Spain - April 13 - 17, 2015, pp. 1933–1939 Conference
DOI URL BibTeX
@inproceedings{sac15,
isbn = {978-1-4503-3196-8},
publisher = {ACM},
editor = {Roger L. Wainwright and
Juan Manuel Corchado and
Alessio Bechini and
Jiman Hong},
doi = {10.1145/2695664.2695819},
url = {http://doi.acm.org/10.1145/2695664.2695819},
optannote = {},
note = {Short paper},
optpublisher = {},
optorganization = {},
optmonth = {},
optaddress = {},
optseries = {},
optnumber = {},
optvolume = {},
opteditor = {},
optyear = {},
optpages = {},
optbooktitle = {},
optkey = {},
optcrossref = {},
metrics = {rank B, acceptance rate 24%},
pages = {1933--1939},
year = {2015},
booktitle = {30th ACM/SIGAPP Symposium on Applied Computing, SAC 2015, Salamanca, Spain - April 13 - 17, 2015},
title = {Compilation Of Synchronous Observers As Code Contracts},
author = {Arnaud Dieumegard and Pierre-Loic Garoche and Temesghen Kahsai and Alice Tailliar and Xavier Thirioux}
}
Property-based Polynomial Invariant Generation using Sums-of-Squares Optimization
Assale Adje, Pierre-Loic Garoche, Victor Magron
Static Analysis - 22st International Symposium, SAS 2015, St Malo, France, 2015. Proceedings, vol. 9291, pp. 235–251 Conference
DOI BibTeX
@inproceedings{sas15,
optannote = {},
optnote = {},
optpublisher = {},
optorganization = {},
optaddress = {},
optmonth = {},
optpages = {},
optseries = {},
optnumber = {},
optvolume = {},
opteditor = {},
isbn = {978-3-662-48287-2},
volume = {9291},
editor = {Sandrine Blazy and
Thomas Jensen},
doi = {10.1007/978-3-662-48288-9_14},
optcrossref = {},
pages = {235--251},
optyear = {},
optbooktitle = {},
year = {2015},
metrics = {rank A, acceptance rate 40%},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
booktitle = {Static Analysis - 22st International Symposium, SAS 2015, St Malo,
France, 2015. Proceedings},
optkey = {},
title = {Property-based Polynomial Invariant Generation using Sums-of-Squares Optimization},
author = {Assale Adje and Pierre-Loic Garoche and Victor Magron}
}
Quadratic Zonotopes - An Extension of Zonotopes to Quadratic Arithmetics
Assalé Adjé, Pierre-Loïc Garoche, Alexis Werey
Programming Languages and Systems - 13th Asian Symposium, APLAS 2015, Pohang, South Korea, November 30 - December 2, 2015, Proceedings, pp. 127–145 Conference
DOI BibTeX
@inproceedings{aplas15,
bibsource = {dblp computer science bibliography, http://dblp.org},
biburl = {http://dblp.uni-trier.de/rec/bib/conf/aplas/AdjeGW15},
timestamp = {Wed, 09 Dec 2015 19:21:03 +0100},
doi = {10.1007/978-3-319-26529-2_8},
year = {2015},
pages = {127--145},
booktitle = {Programming Languages and Systems - 13th Asian Symposium, APLAS
2015, Pohang, South Korea, November 30 - December 2, 2015, Proceedings},
title = {Quadratic Zonotopes - An Extension of Zonotopes to Quadratic Arithmetics},
author = {Assalé Adjé and
Pierre-Loïc Garoche and
Alexis Werey},
metrics = {rank B, acceptance rate 32%s}
}
A Sums-of-Squares Extension of Policy Iterations
Assalé Adjé, Pierre-Loïc Garoche, Victor Magron
Technical Report, vol. abs/1503.08090, 2015 Tech report
URL BibTeX
@techreport{DBLP:journals/corr/AdjeGM15a,
bibsource = {dblp computer science bibliography, http://dblp.org},
biburl = {http://dblp.uni-trier.de/rec/bib/journals/corr/AdjeGM15a},
timestamp = {Thu, 09 Apr 2015 01:00:00 +0200},
url = {http://arxiv.org/abs/1503.08090},
year = {2015},
volume = {abs/1503.08090},
journal = {CoRR},
title = {A Sums-of-Squares Extension of Policy Iterations},
author = {Assalé Adjé and
Garoche, Pierre-Loïc and
Victor Magron}
}
Formal specification of Projet P toolset requirements - SP5.T4
Project P consortium
Technical Report, 2015 Tech report
BibTeX
@techreport{SP5T4,
optannote = {},
note = {21 pages},
optmonth = {},
optaddress = {},
optnumber = {},
opttype = {},
optkey = {},
year = {2015},
institution = {},
title = {Formal specification of Projet P toolset requirements - SP5.T4},
author = {Project P consortium}
}
Projet CAFEIN - Rapport avancement RA 3/21071
Pierre-Loïc Garoche
Technical Report, Onera, 2015 Tech report
BibTeX
@techreport{CAFEIN-RA3,
optannote = {},
note = {11 pages},
optmonth = {},
optaddress = {},
optnumber = {},
opttype = {},
optkey = {},
year = {2015},
institution = {Onera},
title = {Projet CAFEIN - Rapport avancement RA 3/21071},
author = {Garoche, Pierre-Loïc}
}
Property-based Polynomial Invariant Generation using Sums-of-Squares Optimization
Assalé Adjé, Pierre-Loïc Garoche, Victor Magron
Technical Report, vol. abs/1503.07025, 2015 Tech report
URL BibTeX
@techreport{DBLP:journals/corr/AdjeGM15,
bibsource = {dblp computer science bibliography, http://dblp.org},
biburl = {http://dblp.uni-trier.de/rec/bib/journals/corr/AdjeGM15},
timestamp = {Thu, 09 Apr 2015 01:00:00 +0200},
url = {http://arxiv.org/abs/1503.07025},
year = {2015},
volume = {abs/1503.07025},
journal = {CoRR},
title = {Property-based Polynomial Invariant Generation using Sums-of-Squares
Optimization},
author = {Assalé Adjé and
Garoche, Pierre-Loïc and
Victor Magron}
}
2014 (10)
Computing Quadratic Invariants with Min- and Max-Policy Iterations: A Practical Comparison
Pierre Roux, Pierre-Loïc Garoche
FM 2014: Formal Methods - 19th International Symposium, Singapore, May 12-16, 2014. Proceedings, pp. 563–578 Conference
DOI BibTeX
@inproceedings{DBLP:conf/fm/RouxG14,
metrics = {rank A, acceptance rate 25%},
bibsource = {dblp computer science bibliography, http://dblp.org},
biburl = {http://dblp.uni-trier.de/rec/bib/conf/fm/RouxG14},
timestamp = {Wed, 14 May 2014 21:14:55 +0200},
doi = {10.1007/978-3-319-06410-9_38},
crossref = {DBLP:conf/fm/2014},
year = {2014},
pages = {563--578},
booktitle = {FM 2014: Formal Methods - 19th International Symposium, Singapore,
May 12-16, 2014. Proceedings},
title = {Computing Quadratic Invariants with Min- and Max-Policy Iterations:
A Practical Comparison},
author = {Pierre Roux and
Garoche, Pierre-Loïc}
}
Synthesizing Modular Invariants for Synchronous Code
Pierre-Loïc Garoche, Arie Gurfinkel, Temesghen Kahsai
Proceedings First Workshop on Horn Clauses for Verification and Synthesis, HCVS 2014, Vienna, Austria, 17 July 2014., pp. 19–30 Conference
DOI BibTeX
@inproceedings{DBLP:journals/corr/GarocheGK14,
bibsource = {dblp computer science bibliography, http://dblp.org},
biburl = {http://dblp.uni-trier.de/rec/bib/journals/corr/GarocheGK14},
timestamp = {Mon, 05 Jan 2015 16:52:15 +0100},
doi = {10.4204/EPTCS.169.4},
optcrossref = {DBLP:journals/corr/BjornerFRS14},
year = {2014},
pages = {19--30},
booktitle = {Proceedings First Workshop on Horn Clauses for Verification and Synthesis,
HCVS 2014, Vienna, Austria, 17 July 2014.},
title = {Synthesizing Modular Invariants for Synchronous Code},
author = {Garoche, Pierre-Loïc and
Arie Gurfinkel and
Temesghen Kahsai}
}
Testing-Based Compiler Validation for Synchronous Languages
Pierre-Loïc Garoche, Falk Howar, Temesghen Kahsai, Xavier Thirioux
NASA Formal Methods - 6th International Symposium, NFM 2014, Houston, TX, USA, April 29 - May 1, 2014. Proceedings, pp. 246–251 Conference
DOI BibTeX
@inproceedings{DBLP:conf/nfm/GarocheHKT14,
bibsource = {dblp computer science bibliography, http://dblp.org},
biburl = {http://dblp.uni-trier.de/rec/bib/conf/nfm/GarocheHKT14},
note = {Short paper},
timestamp = {Fri, 25 Apr 2014 14:20:46 +0200},
doi = {10.1007/978-3-319-06200-6_19},
crossref = {DBLP:conf/nfm/2014},
year = {2014},
pages = {246--251},
metrics = {acceptance rate 35%},
booktitle = {NASA Formal Methods - 6th International Symposium, NFM 2014, Houston,
TX, USA, April 29 - May 1, 2014. Proceedings},
title = {Testing-Based Compiler Validation for Synchronous Languages},
author = {Garoche, Pierre-Loïc and
Falk Howar and
Temesghen Kahsai and
Xavier Thirioux}
}
Automatic Synthesis of Piecewise Linear Quadratic Invariants for Programs
Assalé Adjé, Pierre-Loïc Garoche
Technical Report, vol. abs/1409.5089, 2014 Tech report
URL BibTeX
@techreport{DBLP:journals/corr/AdjeG14,
bibsource = {dblp computer science bibliography, http://dblp.org},
biburl = {http://dblp.uni-trier.de/rec/bib/journals/corr/AdjeG14},
timestamp = {Mon, 01 Dec 2014 00:00:00 +0100},
url = {http://arxiv.org/abs/1409.5089},
year = {2014},
volume = {abs/1409.5089},
journal = {CoRR},
title = {Automatic Synthesis of Piecewise Linear Quadratic Invariants for Programs},
author = {Assalé Adjé and
Garoche, Pierre-Loïc}
}
Credible Autocoding of Convex Optimization Algorithms
Timothy Wang, Romain Jobredeaux, Marc Pantel, Pierre-Loïc Garoche, Eric Feron et al.
Technical Report, vol. abs/1403.1861, 2014 Tech report
URL BibTeX
@techreport{DBLP:journals/corr/WangJPGFH14,
bibsource = {dblp computer science bibliography, http://dblp.org},
biburl = {http://dblp.uni-trier.de/rec/bib/journals/corr/WangJPGFH14},
timestamp = {Tue, 01 Apr 2014 01:00:00 +0200},
url = {http://arxiv.org/abs/1403.1861},
year = {2014},
volume = {abs/1403.1861},
journal = {CoRR},
title = {Credible Autocoding of Convex Optimization Algorithms},
author = {Timothy Wang and
Romain Jobredeaux and
Marc Pantel and
Garoche, Pierre-Loïc and
Eric Feron and
Didier Henrion}
}
Open-loop analysis of the control program: first proposal WP2 D2.1
CAFEIN project consortium
Technical Report, 2014 Tech report
BibTeX
@techreport{CAFEIND2.1,
optannote = {},
note = {35 pages},
optmonth = {},
optaddress = {},
optnumber = {},
opttype = {},
optkey = {},
year = {2014},
institution = {},
title = {Open-loop analysis of the control program: first proposal WP2 D2.1},
author = {CAFEIN project consortium}
}
Preliminary report on clock directed verification and invariant generation WP1 D1.1
CAFEIN project consortium
Technical Report, 2014 Tech report
BibTeX
@techreport{CAFEIND1.1,
optannote = {},
note = {54 pages},
optmonth = {},
optaddress = {},
optnumber = {},
opttype = {},
optkey = {},
year = {2014},
institution = {},
title = {Preliminary report on clock directed verification and invariant generation WP1 D1.1},
author = {CAFEIN project consortium}
}
Projet CAFEIN - Rapport avancement RA 2/21071
Pierre-Loïc Garoche
Technical Report, Onera, 2014 Tech report
BibTeX
@techreport{CAFEIN-RA2,
optannote = {},
note = {12 pages},
optmonth = {},
optaddress = {},
optnumber = {},
opttype = {},
optkey = {},
year = {2014},
institution = {Onera},
title = {Projet CAFEIN - Rapport avancement RA 2/21071},
author = {Garoche, Pierre-Loïc}
}
Quadratic Zonotopes: An extension of Zonotopes to Quadratic Arithmetics
Assalé Adjé, Pierre-Loïc Garoche, Alexis Werey
Technical Report, vol. abs/1411.5847, 2014 Tech report
URL BibTeX
@techreport{DBLP:journals/corr/AdjeGW14,
bibsource = {dblp computer science bibliography, http://dblp.org},
biburl = {http://dblp.uni-trier.de/rec/bib/journals/corr/AdjeGW14},
timestamp = {Mon, 01 Dec 2014 00:00:00 +0100},
url = {http://arxiv.org/abs/1411.5847},
year = {2014},
volume = {abs/1411.5847},
journal = {CoRR},
title = {Quadratic Zonotopes: An extension of Zonotopes to Quadratic Arithmetics},
author = {Assalé Adjé and
Garoche, Pierre-Loïc and
Alexis Werey}
}
Rapport d’avancement Forces3 – 1ère année RA 1/21534
Virginie Wiels, Alexandre Amiez, Rémi Delmas, Pierre-Loïc Garoche, Thomas Loquen et al.
Technical Report, Onera, 2014 Tech report
BibTeX
@techreport{RA1/21534,
optannote = {},
note = {78 pages},
optmonth = {},
optaddress = {},
optnumber = {},
opttype = {},
optkey = {},
year = {2014},
institution = {Onera},
title = {Rapport d'avancement Forces3 – 1ère année RA 1/21534},
author = {Wiels, Virginie and Amiez, Alexandre and Delmas, Rémi and Garoche, Pierre-Loïc and Loquen, Thomas and Noulard, Eric and Pagetti, Claire}
}
2013 (8)
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 et al.
SAE International Journal of Aerospace, vol. 6(1), pp. 150-160, 2013 Journal
DOI BibTeX
@article{sae2013,
optmonth = {},
doi = {10.4271/2013-01-2109},
pages = {150-160},
number = {1},
volume = {6},
year = {2013},
journal = {SAE International Journal of Aerospace},
title = {Formal Methods for the Analysis of Critical Control Systems Models: Combining Non-Linear and Linear Analyses},
author = {Adrien Champion and Rémi Delmas and Michael Dierkes and Garoche, Pierre-Loïc and Romain Jobredeaux and Pierre Roux}
}
A Polynomial Template Abstract Domain based on Bernstein Polynomials
Pierre Roux, Pierre-Loïc Garoche
Numerical Software Verification, 2013 Conference
BibTeX
@inproceedings{nsv13,
optannote = {},
optnote = {},
optpublisher = {},
optorganization = {},
optaddress = {},
optmonth = {},
optpages = {},
optseries = {},
optnumber = {},
optvolume = {},
opteditor = {},
optyear = {},
optbooktitle = {},
optkey = {},
optcrossref = {},
year = {2013},
booktitle = {Numerical Software Verification},
title = {A Polynomial Template Abstract Domain based on Bernstein Polynomials},
author = {Roux, Pierre and Garoche, Pierre-Loïc}
}
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 et al.
Formal Methods for Industrial Critical Systems (FMICS’13), vol. 8187, pp. 1-16, 2013 Conference
DOI BibTeX
@inproceedings{fmics13,
metrics = {acceptance rate 52%},
optannote = {},
note = {\textbfBest paper award},
optpublisher = {},
optorganization = {},
optaddress = {},
optmonth = {},
pages = {1-16},
optseries = {},
optnumber = {},
optvolume = {},
isbn = {978-3-642-41009-3},
volume = {8187},
editor = {Charles Pecheur and
Michael Dierkes},
doi = {10.1007/978-3-642-41010-9_1},
opteditor = {},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
year = {2013},
booktitle = {Formal Methods for Industrial Critical Systems (FMICS'13)},
optkey = {},
optcrossref = {},
title = {Formal Methods for the Analysis of Critical Control Systems Models: Combining Non-Linear and Linear Analyses},
author = {Adrien Champion and Rémi Delmas and Michael Dierkes and Garoche, Pierre-Loïc and Romain Jobredeaux and Pierre Roux}
}
Incremental Invariant Generation Using Logic-Based Automatic Abstract Transformers
Pierre-Loïc Garoche, Temesghen Kahsai, Cesare Tinelli
NASA Formal Methods - Fifth International Symposium, NFM 2013, Moffett Field, CA USA, May 14-16, 2013. Proceedings, vol. 7871, pp. 139-154 Conference
DOI BibTeX
@inproceedings{nfm13,
isbn = {978-3-642-38087-7},
volume = {7871},
doi = {10.1007/978-3-642-38088-4_10},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Brat, Guillaume and Rungta, Neha and Venet, Arnaud},
metrics = {acceptance rate 37%},
booktitle = {NASA Formal Methods - Fifth International Symposium, NFM
2013, Moffett Field, CA USA, May 14-16, 2013. Proceedings},
bibsource = {DBLP, http://dblp.uni-trier.de},
pages = {139-154},
year = {2013},
title = {Incremental Invariant Generation Using Logic-Based Automatic
Abstract Transformers},
author = {Garoche, Pierre-Loïc and
Temesghen Kahsai and
Cesare Tinelli}
}
Integrating Policy Iterations in Abstract Interpreters
Pierre Roux, Pierre-Loïc Garoche
pp. 240-254, 2013 Conference
DOI BibTeX
@inproceedings{atva13,
doi = {10.1007/978-3-319-02444-8_18},
metrics = {rank A, acceptance rate 36%},
bibsource = {DBLP, http://dblp.uni-trier.de},
optcrossref = {DBLP:conf/atva/2013},
pages = {240-254},
year = {2013},
optbooktitle = {ATVA},
title = {Integrating Policy Iterations in Abstract Interpreters},
author = {Pierre Roux and
Garoche, Pierre-Loïc}
}
Formal methods in project P - SP5.L2
Project P consortium
Technical Report, 2013 Tech report
BibTeX
@techreport{SP5L2,
optannote = {},
note = {17 pages},
optmonth = {},
optaddress = {},
optnumber = {},
opttype = {},
optkey = {},
year = {2013},
institution = {},
title = {Formal methods in project P - SP5.L2},
author = {Project P consortium}
}
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 et al.
Technical Report, vol. abs/1307.2641, 2013 Tech report
URL BibTeX
@techreport{DBLP:journals/corr/WangJHGDFP13,
bibsource = {dblp computer science bibliography, http://dblp.org},
biburl = {http://dblp.uni-trier.de/rec/bib/journals/corr/WangJHGDFP13},
timestamp = {Thu, 15 Aug 2013 01:00:00 +0200},
url = {http://arxiv.org/abs/1307.2641},
year = {2013},
volume = {abs/1307.2641},
journal = {CoRR},
title = {From Design to Implementation: an Automated, Credible Autocoding Chain
for Control Systems},
author = {Timothy Wang and
Romain Jobredeaux and
Heber Herencia-Zapana and
Garoche, Pierre-Loïc and
Arnaud Dieumegard and
Eric Feron and
Marc Pantel}
}
Projet CAFEIN - Rapport avancement RA 1/21071
Pierre-Loïc Garoche
Technical Report, Onera, 2013 Tech report
BibTeX
@techreport{CAFEIN-RA1,
optannote = {},
note = {8 pages},
optmonth = {},
optaddress = {},
optnumber = {},
opttype = {},
optkey = {},
year = {2013},
institution = {Onera},
title = {Projet CAFEIN - Rapport avancement RA 1/21071},
author = {Garoche, Pierre-Loïc}
}
2012 (11)
Formal Verification of Critical Aerospace Software
Virginie Wiels, Rémi Delmas, David Doose, Pierre-Loic. Garoche, Jacques Cazin et al.
Aerospace Lab Journal, vol. 4, 2012 Journal
URL BibTeX
@article{aerospace12,
optannote = {},
optnote = {},
url = {www.aerospacelab-journal.org/al4/},
month = {5},
optpages = {},
optnumber = {},
volume = {4},
optkey = {},
year = {2012},
journal = {Aerospace Lab Journal},
title = {Formal Verification of Critical Aerospace Software},
author = {Wiels, Virginie and Delmas, Rémi and Doose, David and Garoche, Pierre-Loic. and Cazin, Jacques and Durrieu, Guy}
}
A Generic Ellipsoid Abstract Domain for Linear Time Invariant Systems
Pierre Roux, Romain Jobredeaux, Pierre-Loïc Garoche, Éric Féron
Proceedings of the 15th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2012, Beijing, China, April 17-19, 2012, pp. 105-114 Conference
DOI URL BibTeX
@inproceedings{hscc12,
pages = {105-114},
publisher = {ACM},
year = {2012},
isbn = {978-1-4503-1220-2},
doi = {10.1145/2185632.2185651},
url = {http://doi.acm.org/10.1145/2185632.2185651},
editor = {Dang, Thao and Mitchell, Ian},
metrics = {acceptance rate 60%},
booktitle = {Proceedings of the 15th ACM International Conference on
Hybrid Systems: Computation and Control, HSCC 2012, Beijing, China, April 17-19, 2012},
title = {A Generic Ellipsoid Abstract Domain for Linear Time Invariant Systems},
author = {Roux, Pierre and Jobredeaux, Romain and Garoche, Pierre-Loïc and Féron, Éric}
}
Incremental verification with mode variable invariants in state machines
Temesghen Kahsai, Pierre-Loïc Garoche, Cesare Tinelli, Mike Whalen
NASA Formal Methods - Forth International Symposium, NFM 2012, Norfolk, VA USA, April 3-5, 2012. Proceedings, vol. 7226, pp. 388-402 Conference
DOI BibTeX
@inproceedings{nfm12_1,
doi = {10.1007/978-3-642-28891-3_35},
volume = {7226},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Goodloe, Alwyn and Person, Suzette},
year = {2012},
pages = {388-402},
metrics = {acceptance rate 38%},
booktitle = {NASA Formal Methods - Forth International Symposium, NFM
2012, Norfolk, VA USA, April 3-5, 2012. Proceedings},
author = {Kahsai, Temesghen and Garoche, Pierre-Loïc and Tinelli, Cesare and Whalen, Mike},
title = {Incremental verification with mode variable invariants in state machines}
}
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 Féron et al.
NASA Formal Methods - Forth International Symposium, NFM 2012, Norfolk, VA USA, April 3-5, 2012. Proceedings, vol. 7226, pp. 147-161 Conference
DOI BibTeX
@inproceedings{nfm12_2,
series = {Lecture Notes in Computer Science},
volume = {7226},
publisher = {Springer},
editor = {Goodloe, Alwyn and Person, Suzette},
year = {2012},
doi = {10.1007/978-3-642-28891-3_15},
pages = {147-161},
metrics = {acceptance rate 38%},
booktitle = {NASA Formal Methods - Forth International Symposium, NFM
2012, Norfolk, VA USA, April 3-5, 2012. Proceedings},
author = {Herencia-Zapana, Heber and Jobredeaux, Romain and Owre, Sam and Garoche, Pierre-Loïc and Féron, Eric and Perez, Gilberto and Ascariz, Pablo},
title = {PVS Linear Algebra Libraries for Verification of Control Software Algorithms in C/ACSL}
}
CAVALE - Intégration dans les processus de validation - focus sur les propriétés fonctionnelle. RF 4/14888
Pierre-Loïc Garoche
Technical Report, Onera, 2012 Tech report
BibTeX
@techreport{RF4/14888,
optannote = {},
note = {46 pages},
optmonth = {},
optaddress = {},
optnumber = {},
opttype = {},
optkey = {},
year = {2012},
institution = {Onera},
title = {CAVALE - Intégration dans les processus de validation - focus sur les propriétés fonctionnelle. RF 4/14888},
author = {Garoche, Pierre-Loïc}
}
Invariant stream generators using automatic abstract transformers based on a decidable logic
Pierre-Loïc Garoche, Temesghen Kahsai, Cesare Tinelli
Technical Report, vol. abs/1205.3758, 2012 Tech report
URL BibTeX
@techreport{DBLP:journals/corr/abs-1205-3758,
bibsource = {dblp computer science bibliography, http://dblp.org},
biburl = {http://dblp.uni-trier.de/rec/bib/journals/corr/abs-1205-3758},
timestamp = {Wed, 10 Oct 2012 01:00:00 +0200},
url = {http://arxiv.org/abs/1205.3758},
year = {2012},
volume = {abs/1205.3758},
journal = {CoRR},
title = {Invariant stream generators using automatic abstract transformers
based on a decidable logic},
author = {Garoche, Pierre-Loïc and
Temesghen Kahsai and
Cesare Tinelli}
}
Kind,a k-induction based model-checker
Pierre-Loïc Garoche, Temesghen Kasai, Cesare Tinelli
collaboration avec l’Univ. of Iowa, 2012– Software
URL BibTeX
@electronic{kind,
url = {http://clc.cs.uiowa.edu/Kind/},
note = {collaboration avec l'Univ. of Iowa},
title = {Kind,a k-induction based model-checker},
year = {2012--},
date-modified = {2007-12-12 21:25:19 +0100},
date-added = {2007-12-12 21:24:26 +0100},
author = {Garoche, Pierre-Loïc and Kasai, Temesghen and Tinelli, Cesare}
}
Kind-AI, automatic abstract interpreter module for Lustre model-checker Kind
Pierre-Loïc Garoche, Temesghen Kasai, Cesare Tinelli
collaboration avec l’Univ. of Iowa, 2012 Software
URL BibTeX
@electronic{kind-ai,
url = {http://clc.cs.uiowa.edu/Kind/NFM13/},
year = {2012},
note = {collaboration avec l'Univ. of Iowa},
title = {Kind-AI, automatic abstract interpreter module for Lustre model-checker Kind},
date-modified = {2007-12-12 21:25:19 +0100},
date-added = {2007-12-12 21:24:26 +0100},
author = {Garoche, Pierre-Loïc and Kasai, Temesghen and Tinelli, Cesare}
}
LustreC: a modular Lustre compiler
Pierre-Loïc Garoche, Xavier Thiroux, Temesghen Kahsai
collaboration avec l’IRIT et NASA Ames, 2012– Software
URL BibTeX
@electronic{lustrec,
url = {https://github.com/coco-team/lustrec},
year = {2012--},
note = {collaboration avec l'IRIT et NASA Ames},
title = {LustreC: a modular Lustre compiler},
author = {Garoche, Pierre-Loïc and Thiroux, Xavier and Kahsai, Temesghen}
}
Ocaml library for Semi-Definite Programming (SDP, SOS)
Pierre Roux, Pierre-Loïc Garoche
2012– Software
URL BibTeX
@electronic{osdp,
year = {2012--},
url = {https://cavale.enseeiht.fr/osdp/},
title = {Ocaml library for Semi-Definite Programming (SDP, SOS)},
author = {Roux, Pierre and Garoche, Pierre-Loïc}
}
TINY: Simple Static Analyzer for Imperative Code and Numerical precision analysis
Pierre Roux, Pierre-Loïc Garoche, Alexis Werey
2012– Software
URL BibTeX
@electronic{tiny,
url = {https://cavale.enseeiht.fr/QuadZonotopes/},
year = {2012--},
title = {TINY: Simple Static Analyzer for Imperative Code and Numerical precision analysis},
author = {Roux, Pierre and Garoche, Pierre-Loïc and Werey, Alexis}
}
2011 (5)
Towards Cooperation of Formal Methods for the Analysis of Critical Control Systems
Adrien Champion, Rémi Delmas, Pierre-Loïc Garoche, Pierre Roux
SAE International Journal of Aerospace, vol. 4(2), pp. 850-858, 2011 Journal
DOI BibTeX
@article{sae2011,
doi = {10.4271/2011-01-2558},
optannote = {},
note = {\textbfArch T. Colwell Merit Award},
month = {11},
pages = {850-858},
number = {2},
volume = {4},
year = {2011},
journal = {SAE International Journal of Aerospace},
title = {Towards Cooperation of Formal Methods for the Analysis of Critical Control Systems},
author = {Champion, Adrien and Delmas, Rémi and Garoche, Pierre-Loïc and Roux, Pierre}
}
Dessine moi un domaine abstrait fini – une recette à base de Camlp4 et de solveurs SMT
Pierre Roux, Pierre-Loïc Garoche
22èmes Journées Francophones des Langages Applicatifs (JFLA 2011), La Bresse, France, pp. 242-268 Conference
URL BibTeX
@inproceedings{jfla2011,
url = {http://studia.complexica.net/Art/AC-JFLA11-09.pdf},
year = {2011},
series = {Studia Informatica Universalis},
title = {Dessine moi un domaine abstrait fini -- une recette à base de Camlp4 et de solveurs SMT},
pages = {242-268},
editor = {Éditions Hermann},
booktitle = {22èmes Journées Francophones des Langages Applicatifs (JFLA 2011), La Bresse, France},
author = {Pierre Roux and Garoche, Pierre-Loïc}
}
A Generic Ellipsoid Abstract Domain for Linear Time Invariant Systems
Pierre Roux, Romain Jobredeaux, Pierre-Loïc Garoche, Eric Féron
Technical Report, 2011 Tech report
URL PDF BibTeX
@techreport{roux:hal-00608673,
hal_version = {v2},
hal_id = {hal-00608673},
month = {5},
year = {2011},
url = {https://hal.archives-ouvertes.fr/hal-00608673},
author = {Roux, Pierre and Jobredeaux, Romain and Garoche, Pierre-Loïc and Féron, Eric},
title = {A Generic Ellipsoid Abstract Domain for Linear Time Invariant Systems}
}
CAVALE - Collaboration d’analyses - Choix techniques & Mise en oeuvre. RT 3/14888
Pierre-Loïc Garoche
Technical Report, Onera, 2011 Tech report
BibTeX
@techreport{RT3/14888,
optannote = {},
note = {42 pages},
optmonth = {},
optaddress = {},
optnumber = {},
opttype = {},
optkey = {},
year = {2011},
institution = {Onera},
title = {CAVALE - Collaboration d'analyses - Choix techniques & Mise en oeuvre. RT 3/14888},
author = {Garoche, Pierre-Loïc}
}
SMT-AI, abstract interpreter for a temporal extension of SMT-lib
Pierre-Loïc Garoche, Pierre Roux
utilisé en recherche et enseignement, 2011– Software
URL BibTeX
@electronic{smt-ai,
url = {https://cavale.enseeiht.fr/smt-ai/},
note = {utilisé en recherche et enseignement},
year = {2011--},
title = {SMT-AI, abstract interpreter for a temporal extension of SMT-lib},
date-modified = {2007-12-12 21:25:19 +0100},
date-added = {2007-12-12 21:24:26 +0100},
author = {Garoche, Pierre-Loïc and Roux, Pierre}
}
2010 (3)
SMT-AI: an Abstract Interpreter for a Synchronous Extension of SMT-lib
Pierre Roux, Rémi Delmas, Pierre-Loïc Garoche
1st International Workshop on Tools for Automatic Program AnalysiS (TAPAS 2010), SAS’10 satellite event, Perpignan, France, vol. 267(2), pp. 55–68 Conference
DOI BibTeX
@inproceedings{tapas10,
bibsource = {dblp computer science bibliography, http://dblp.org},
biburl = {http://dblp.uni-trier.de/rec/bib/journals/entcs/RouxDG10},
timestamp = {Wed, 29 Dec 2010 17:29:59 +0100},
doi = {10.1016/j.entcs.2010.09.018},
year = {2010},
pages = {55--68},
number = {2},
volume = {267},
publisher = {Elsevier Electr. Notes Theor. Comput. Sci.},
title = {SMT-AI: an Abstract Interpreter for a Synchronous Extension of SMT-lib},
month = {9},
editor = {Delmas, David and Rival, Xavier},
booktitle = {1st International Workshop on Tools for Automatic Program AnalysiS (TAPAS 2010), SAS'10 satellite event, Perpignan, France},
author = {Pierre Roux and Rémi Delmas and Garoche, Pierre-Loïc}
}
2.1 - Modélisation pour la prise en compte des phénomènes de rayonnements dans les architectures logicielles avioniques. RT 1/16764
Guy Durrieu, Pierre-Loïc Garoche Frédéric Boniol
Technical Report, Onera, 2010 Tech report
BibTeX
@techreport{RT1/16764,
optannote = {},
note = {55 pages},
optmonth = {},
optaddress = {},
optnumber = {},
opttype = {},
optkey = {},
year = {2010},
institution = {Onera},
title = {2.1 - Modélisation pour la prise en compte des phénomènes de rayonnements dans les architectures logicielles avioniques. RT 1/16764},
author = {Frédéric Boniol, Guy Durrieu, Pierre-Loïc Garoche}
}
CAVALE - Collaboration d’analyses pour la vérification d’erreurs à l’exécution. RT 2/14888
Pierre-Loïc Garoche
Technical Report, Onera, 2010 Tech report
BibTeX
@techreport{RT2/14888,
optannote = {},
note = {37 pages},
optmonth = {},
optaddress = {},
optnumber = {},
opttype = {},
optkey = {},
year = {2010},
institution = {Onera},
title = {CAVALE - Collaboration d'analyses pour la vérification d'erreurs à l'exécution. RT 2/14888},
author = {Garoche, Pierre-Loïc}
}
2009 (6)
Essay on Semantics Definition in MDE - An Instrumented Approach for Model Verification
Benoît Combemale, Xavier Crégut, Pierre-Loïc Garoche, Xavier Thirioux
Journal of Software (JSW), vol. 4(9), pp. 943-958, 2009 Journal
DOI BibTeX
@article{jsw09,
bibsource = {DBLP, http://dblp.uni-trier.de},
doi = {10.4304/jsw.4.9.943-958},
publisher = {Academy Publisher},
pages = {943-958},
year = {2009},
number = {9},
volume = {4},
journal = {Journal of Software (JSW)},
title = {Essay on Semantics Definition in MDE - An Instrumented Approach
for Model Verification},
author = {Benoît Combemale and
Xavier Crégut and
Garoche, Pierre-Loïc and
Xavier Thirioux}
}
ASBAPROD Assurance Basée Produit - Rapport final, RF 4/13733
Jacques Cazin, Pierre-Loïc Garoche, Virginie Wiels
Technical Report, Onera, 2009 Tech report
BibTeX
@techreport{RF4/13733,
optannote = {},
note = {637 pages},
optmonth = {},
optaddress = {},
optnumber = {},
opttype = {},
optkey = {},
year = {2009},
institution = {Onera},
title = {ASBAPROD Assurance Basée Produit - Rapport final, RF 4/13733},
author = {Cazin, Jacques and Garoche, Pierre-Loïc and Wiels, Virginie}
}
CAVALE - Etat de l’art. RT 1/14888
Pierre-Loïc Garoche
Technical Report, Onera, 2009 Tech report
BibTeX
@techreport{RT1/14888,
optannote = {},
note = {27 pages},
optmonth = {},
optaddress = {},
optnumber = {},
opttype = {},
optkey = {},
year = {2009},
institution = {Onera},
title = {CAVALE - Etat de l'art. RT 1/14888},
author = {Garoche, Pierre-Loïc}
}
Impacts of static analysis on current development process - D2.2.1 ES-PASS Project. RT 1/13009
Pierre-Loïc Garoche, Virginie Wiels Jacques Cazin
Technical Report, Onera, 2009 Tech report
BibTeX
@techreport{RT1/13009,
optannote = {},
note = {26 pages},
optmonth = {},
optaddress = {},
optnumber = {},
opttype = {},
optkey = {},
year = {2009},
institution = {Onera},
title = {Impacts of static analysis on current development process - D2.2.1 ES-PASS Project. RT 1/13009},
author = {Jacques Cazin, Pierre-Loïc Garoche, Virginie Wiels}
}
New development processes - D2.4.1 ES-PASS Project. RT 2/13009
Pierre-Loïc Garoche, Virginie Wiels Jacques Cazin
Technical Report, Onera, 2009 Tech report
BibTeX
@techreport{RT2/13009,
optannote = {},
note = {24 pages},
optmonth = {},
optaddress = {},
optnumber = {},
opttype = {},
optkey = {},
year = {2009},
institution = {Onera},
title = {New development processes - D2.4.1 ES-PASS Project. RT 2/13009},
author = {Jacques Cazin, Pierre-Loïc Garoche, Virginie Wiels}
}
Qualifiation of tools - D2.5.1 ES-PASS Project. RT 3/13009
Jacques Cazin, Xavier Crégut, Pierre-Loïc Garoche, Marc Pantel, Virginie Wiels
Technical Report, Onera, 2009 Tech report
BibTeX
@techreport{RT/3.13009,
optannote = {},
note = {14 pages},
optmonth = {},
optaddress = {},
optnumber = {},
opttype = {},
optkey = {},
year = {2009},
institution = {Onera},
title = {Qualifiation of tools - D2.5.1 ES-PASS Project. RT 3/13009},
author = {Jacques Cazin and Xavier Crégut and Pierre-Loïc Garoche and Marc Pantel and Virginie Wiels}
}
2008 (4)
A Property-Driven Approach to Formal Verification of Process Models
Benoit Combemale, Xavier Crégut, Pierre-Loïc Garoche, Xavier Thirioux, François Vernadat
Enterprise Information Systems, vol. 12, pp. 286-300, 2008 Book chapter
DOI BibTeX
@inbook{eis07_2,
year = {2008},
title = {A Property-Driven Approach to Formal Verification of Process Models},
publisher = {Springer Verlag},
language = {English},
isbn = {978-3-540-88709-6},
doi = {10.1007/978-3-540-88710-2_23},
pages = {286-300},
series = {Lecture Notes in Business Information Processing},
volume = {12},
editor = {Filipe, Joaquim and Cordeiro, José and Cardoso, Jorge},
booktitle = {Enterprise Information Systems},
date-modified = {2007-12-11 15:42:54 +0100},
date-added = {2007-12-11 15:08:08 +0100},
author = {Combemale, Benoit and Crégut, Xavier and Garoche, Pierre-Loïc and Thirioux, Xavier and Vernadat, François}
}
ASBAPROD - Mise en oeuvre systématique de l’approche sur la Phase 1, RT 3/13733
Jacques Cazin, Pierre-Loïc Garoche, Virginie Wiels
Technical Report, Onera, 2008 Tech report
BibTeX
@techreport{RT3/13733,
optannote = {},
note = {27 pages},
optmonth = {},
optaddress = {},
optnumber = {},
opttype = {},
optkey = {},
year = {2008},
institution = {Onera},
title = {ASBAPROD - Mise en oeuvre systématique de l'approche sur la Phase 1, RT 3/13733},
author = {Cazin, Jacques and Garoche, Pierre-Loïc and Wiels, Virginie}
}
Assurance basée sur le produit (ASBAPROD), RT 2/13733
Jacques Cazin, Pierre-Loïc Garoche, Virginie Wiels
Technical Report, Onera, 2008 Tech report
BibTeX
@techreport{RT2/13733,
optannote = {},
note = {26 pages},
optmonth = {},
optaddress = {},
optnumber = {},
opttype = {},
optkey = {},
year = {2008},
institution = {Onera},
title = {Assurance basée sur le produit (ASBAPROD), RT 2/13733 },
author = {Cazin, Jacques and Garoche, Pierre-Loïc and Wiels, Virginie}
}
Static analysis of an actor-based process calculus by abstract interpretation
Pierre-Loïc Garoche
University of Toulouse, INPT, 2008 PhD thesis
BibTeX
@phdthesis{phd,
optannote = {},
optnote = {},
month = {june},
optaddress = {},
opttype = {},
optkey = {},
year = {2008},
school = {University of Toulouse, INPT},
title = {Static analysis of an actor-based process calculus by abstract interpretation},
author = {Garoche, Pierre-Loïc}
}
2007 (6)
Abstract Interpretation-based Static Safety for Actors
Pierre-Loïc Garoche, Marc Pantel, Xavier Thirioux
Journal of Software (JSW), vol. 2(3), pp. 87-98, 2007 Journal
URL BibTeX
@article{jsw07,
year = {2007},
volume = {2},
url = {http://www.academypublisher.com/jsw/vol02/no03/jsw02038798.pdf},
title = {Abstract Interpretation-based Static Safety for Actors},
read = {Yes},
rating = {0},
publisher = {Academy Publisher},
pages = {87-98},
number = {3},
month = {9},
optkeywords = {abstract interpretation, concurrent calculus, actor model, safety analyzes},
journal = {Journal of Software (JSW)},
issn = {1796-217X},
date-modified = {2007-12-11 15:42:54 +0100},
date-added = {2007-09-17 15:20:30 +0200},
author = {Garoche, Pierre-Loïc and Pantel, Marc and Thirioux, Xavier}
}
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
A Property-Driven Approach to Formal Verification of Process Models, pp. 286-300, 2007 Book chapter
DOI BibTeX
@inbook{eis07,
bibsource = {DBLP, http://dblp.uni-trier.de},
doi = {10.1007/978-3-540-88710-2_23},
pages = {286-300},
year = {2007},
title = {A Property-Driven Approach to Formal Verification of Process
Models},
author = {Benoît Combemale and
Xavier Crégut and
Garoche, Pierre-Loïc and
Xavier Thirioux and
François Vernadat}
}
A Framework to formalise the MDE Foundations
Xavier Thirioux, Benoit Combemale, Xavier Crégut, Pierre-Loïc Garoche
International Workshop on Towers of Models (TOWERS’07), co-located with TOOLS’07, Zurich, 25/06/07, pp. 14–30, 2007 Conference
BibTeX
@inproceedings{towers07,
year = {2007},
title = {A Framework to formalise the MDE Foundations},
publisher = {ETH Zurich Technical Report},
pages = {14--30},
month = {6},
language = {anglais},
editor = {Paige, Richard and Bézivin, Jean},
date-modified = {2007-12-11 15:42:54 +0100},
date-added = {2007-09-17 15:40:17 +0200},
booktitle = {International Workshop on Towers of Models (TOWERS'07), co-located with TOOLS'07, Zurich, 25/06/07},
author = {Thirioux, Xavier and Combemale, Benoit and Crégut, Xavier and Garoche, Pierre-Loïc}
}
Expérimentation pour la définition d’une sémantique dans l’IDM
Benoit Combemale, Xavier Crégut, Pierre-Loïc Garoche, Xavier Thirioux
Sémantique des (meta)Modèles, Toulouse, France, 29/01/07, pp. 146–161, 2007 Conference
BibTeX
@inproceedings{semo07,
year = {2007},
title = {Expérimentation pour la définition d'une sémantique dans l'IDM},
publisher = {INPT Research Report},
pages = {146--161},
month = {3},
language = {français},
date-modified = {2007-12-11 15:42:54 +0100},
date-added = {2007-09-17 15:45:28 +0200},
booktitle = {Sémantique des (meta)Modèles, Toulouse, France, 29/01/07},
author = {Combemale, Benoit and Crégut, Xavier and Garoche, Pierre-Loïc and Thirioux, Xavier}
}
Spécification et Vérification par Interprétation Abstraite d’Aspects pour la Distribution
Pierre-Loïc Garoche, Marc Pantel, Xavier Thirioux
Formalisation des Activités Concurrentes (FAC’07), Toulouse, 15–16 March 2007, pp. 1–11 Conference
URL BibTeX
@inproceedings{fac07,
url = {http://seminaire-verif.enseeiht.fr/FAC/2007/Papiers/41.pdf},
pages = {1--11},
year = {2007},
title = {Spécification et Vérification par Interprétation Abstraite d'Aspects pour la Distribution},
publisher = {CNRS Feria - SVF group},
date-modified = {2007-12-11 15:42:54 +0100},
date-added = {2007-09-17 15:52:06 +0200},
booktitle = {Formalisation des Activités Concurrentes (FAC'07), Toulouse, 15--16 March 2007},
author = {Garoche, Pierre-Loïc and Pantel, Marc and Thirioux, Xavier}
}
Towards a Formal Verification of Process Model’s Properties - SimplePDL and TOCL Case Study
Benoit Combemale, Pierre-Loïc Garoche, Xavier Crégut, Xavier Thirioux, François Vernadat
International Conference on Enterprise Information Systems (ICEIS), Funchal, Madeira - Portugal, 12/06/07-16/06/07, pp. 80–89, 2007 Conference
BibTeX
@inproceedings{iceis07,
metrics = {acceptance rate 12%},
year = {2007},
title = {Towards a Formal Verification of Process Model's Properties - SimplePDL and TOCL Case Study},
publisher = {INSTICC Press},
pages = {80--89},
month = {6},
optlanguage = {anglais},
date-modified = {2007-12-11 15:42:54 +0100},
date-added = {2007-09-17 15:44:24 +0200},
booktitle = {International Conference on Enterprise Information Systems (ICEIS), Funchal, Madeira - Portugal, 12/06/07-16/06/07},
author = {Combemale, Benoit and Garoche, Pierre-Loïc and Crégut, Xavier and Thirioux, Xavier and Vernadat, François},
optaddress = {http://www.insticc.net/}
}
2006 (9)
Accurate Centralization for Applying Model Checking on Networked Applications
Cyrille Artho, Pierre-Loïc Garoche
21st IEEE/ACM International Conference on Automated Software Engineering (ASE 2006), 18-22 September 2006, Tokyo, Japan, pp. 177-188 Conference
URL BibTeX
@inproceedings{ase2006,
metrics = {rank A, acceptance rate 17%},
year = {2006},
url = {http://doi.ieeecomputersociety.org/10.1109/ASE.2006.10},
title = {Accurate Centralization for Applying Model Checking on Networked Applications},
publisher = {IEEE Computer Society},
pages = {177-188},
ee = {http://doi.ieeecomputersociety.org/10.1109/ASE.2006.10},
date-modified = {2007-12-11 15:42:54 +0100},
date-added = {2007-09-17 15:29:48 +0200},
booktitle = {21st IEEE/ACM International Conference on Automated Software Engineering (ASE 2006), 18-22 September 2006, Tokyo, Japan},
bibsource = {DBLP, http://dblp.uni-trier.de},
author = {Artho, Cyrille and Garoche, Pierre-Loïc}
}
Adaptive Geographically Bound Mobile Agents
Kenji Tei, Christian Sommer, Yoshiaki Fukazawa, Shinichi Honiden, Pierre-Loïc Garoche
Mobile Ad-hoc and Sensor Networks, vol. 4325, pp. 353-364, 2006 Conference
DOI BibTeX
@inproceedings{msn06,
year = {2006},
volume = {4325},
title = {Adaptive Geographically Bound Mobile Agents},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
pages = {353-364},
doi = {10.1007/11943952_30},
editor = {Cao, Jiannong and Stojmenovic, Ivan and Jia, Xiaohua and Das, Sajal K.},
date-modified = {2007-12-11 15:42:54 +0100},
date-added = {2007-09-17 15:27:17 +0200},
metrics = {acceptance rate 28%},
booktitle = {Mobile Ad-hoc and Sensor Networks},
bibsource = {DBLP, http://dblp.uni-trier.de},
author = {Tei, Kenji and Sommer, Christian and Fukazawa, Yoshiaki and Honiden, Shinichi and Garoche, Pierre-Loïc}
}
Analyse statique d’un calcul d’acteur par interprétation abstraite
Pierre-Loïc Garoche
Colloque des doctorants de l’EDIT, 2006 Conference
BibTeX
@inproceedings{edit06,
year = {2006},
title = {Analyse statique d'un calcul d'acteur par interprétation abstraite},
month = {4},
date-modified = {2007-12-11 15:42:59 +0100},
date-added = {2007-12-11 15:41:21 +0100},
booktitle = {Colloque des doctorants de l'EDIT},
author = {Garoche, Pierre-Loïc}
}
Static Analysis of Actors: From Type Systems to Abstract Interpretation
Pierre-Loïc Garoche, Marc Pantel, Xavier Thirioux
1st International Workshop on Emerging Applications of Abstract Interpretation (EAAI’06), ETAPS’06 satellite event, Vienna, Austria, 2006 Conference
BibTeX
@inproceedings{eaai06,
year = {2006},
title = {Static Analysis of Actors: From Type Systems to Abstract Interpretation},
month = {3},
editor = {Ranzato, Francesco},
date-modified = {2007-12-11 15:42:54 +0100},
date-added = {2007-09-17 15:20:30 +0200},
booktitle = {1st International Workshop on Emerging Applications of Abstract Interpretation (EAAI'06), ETAPS'06 satellite event, Vienna, Austria},
author = {Garoche, Pierre-Loïc and Pantel, Marc and Thirioux, Xavier}
}
Static Safety for an Actor Dedicated Process Calculus by Abstract Interpretation
Pierre-Loïc Garoche, Marc Pantel, Xavier Thirioux
the 8th IFIP International Conference on Formal Methods for Open Object-Based Distributed Systems, Bologna, Italy (FMOODS’06), vol. 4037, pp. 78-92, 2006 Conference
DOI BibTeX
@inproceedings{fmoods06,
metrics = {rank A, acceptance rate 31%},
year = {2006},
volume = {4037},
doi = {10.1007/11768869_8},
title = {Static Safety for an Actor Dedicated Process Calculus by Abstract Interpretation},
series = {Lecture Notes in Computer Science},
publisher = {Springer Verlag},
pages = {78-92},
month = {6},
editor = {Gorrieri, Roberto and Wehrheim, Heike},
date-modified = {2007-12-11 15:42:54 +0100},
date-added = {2007-09-17 15:20:30 +0200},
booktitle = {the 8th IFIP International Conference on Formal Methods for Open Object-Based Distributed Systems, Bologna, Italy (FMOODS'06)},
author = {Garoche, Pierre-Loïc and Pantel, Marc and Thirioux, Xavier}
}
Concern-based Specification and Analysis using Abstract Interpretation - A Distributed Case
Pierre-Loïc Garoche, Marc Pantel, Xavier Thirioux
IRIT Research Report, IRIT, 2006 Tech report
BibTeX
@techreport{rr2006,
year = {2006},
type = {IRIT Research Report},
title = {Concern-based Specification and Analysis using Abstract Interpretation - A Distributed Case},
month = {9},
language = {english},
institution = {IRIT},
date-modified = {2007-12-11 15:42:54 +0100},
date-added = {2007-09-17 15:48:04 +0200},
author = {Garoche, Pierre-Loïc and Pantel, Marc and Thirioux, Xavier}
}
Static Safety for an Actor Dedicated Process Calculus by Abstract Interpretation
Pierre-Loïc Garoche, Marc Pantel, Xavier Thirioux
Technical Report, vol. abs/cs/0611139, 2006 Tech report
URL BibTeX
@techreport{DBLP:journals/corr/abs-cs-0611139,
bibsource = {dblp computer science bibliography, http://dblp.org},
biburl = {http://dblp.uni-trier.de/rec/bib/journals/corr/abs-cs-0611139},
timestamp = {Mon, 05 Dec 2011 00:00:00 +0100},
url = {http://arxiv.org/abs/cs/0611139},
year = {2006},
volume = {abs/cs/0611139},
journal = {CoRR},
title = {Static Safety for an Actor Dedicated Process Calculus by Abstract
Interpretation},
author = {Garoche, Pierre-Loïc and
Marc Pantel and
Xavier Thirioux}
}
YASA: Yet Another Static Analyzer
Pierre-Loïc Garoche, Xavier Thirioux
collaboration avec l’IRIT, utilisé en enseignement, 2006–2011 Software
BibTeX
@electronic{yasa,
year = {2006--2011},
note = {collaboration avec l'IRIT, utilisé en enseignement},
title = {YASA: Yet Another Static Analyzer},
date-modified = {2007-12-12 21:25:34 +0100},
date-added = {2007-12-12 21:23:33 +0100},
author = {Garoche, Pierre-Loïc and Thirioux, Xavier}
}
Zen : an Accurate Centralizer for NASA JavaPathFinder
Pierre-Loïc Garoche, Cyrille Artho
collaboration avec le National Institute of Informatics, Tokyo, 2006 Software
BibTeX
@electronic{zen,
note = {collaboration avec le National Institute of Informatics, Tokyo},
title = {Zen : an Accurate Centralizer for NASA JavaPathFinder},
date-modified = {2007-12-12 21:25:19 +0100},
date-added = {2007-12-12 21:24:26 +0100},
year = {2006},
author = {Garoche, Pierre-Loïc and Artho, Cyrille}
}
2005 (3)
Static Safety for an Actor Dedicated Process Calculus by Abstract Interpretation
Pierre-Loïc Garoche, Marc Pantel, Xavier Thirioux
IRIT Research Report, IRIT, 2005 Tech report
BibTeX
@techreport{rr2005,
year = {2005},
type = {IRIT Research Report},
title = {Static Safety for an Actor Dedicated Process Calculus by Abstract Interpretation},
month = {12},
opykeywords = {actors, abstract interpretation, static analysis},
institution = {IRIT},
date-modified = {2007-12-11 15:42:54 +0100},
date-added = {2007-09-17 15:20:30 +0200},
author = {Garoche, Pierre-Loïc and Pantel, Marc and Thirioux, Xavier}
}
PACSA: a Primitive Actor Calculus Static Analyzer
Pierre-Loïc Garoche
2005–2008 Software
URL BibTeX
@electronic{pacsa,
url = {http://garoche.perso.enseeiht.fr/protos/pacsa/},
year = {2005--2008},
title = {PACSA: a Primitive Actor Calculus Static Analyzer },
date-modified = {2007-12-12 21:24:23 +0100},
date-added = {2007-12-12 21:19:45 +0100},
author = {Garoche, Pierre-Loïc}
}
Static Analysis of Actors by Abstract Interpretation
Pierre-Loïc Garoche
École Normale Supérieure de Cachan, 2005 MSc thesis
BibTeX
@mastersthesis{master,
year = {2005},
title = {Static Analysis of Actors by Abstract Interpretation},
school = {École Normale Supérieure de Cachan},
date-modified = {2007-12-11 15:42:54 +0100},
date-added = {2007-09-17 15:20:30 +0200},
author = {Garoche, Pierre-Loïc}
}