I am currently a researcher at ONERA in Toulouse, France working on static analysis of control command systems (and also of networks). More details about what I did before can be found in this resume (the same in french).
If you really want to see what I can look like, it is here.
Contact
- Pierre Roux, DTIM
ONERA, Centre de Toulouse
BP 74025
2 Avenue Édouard Belin
31055 TOULOUSE CEDEX 4 - phone: (+33)5 62 25 29 05
- pierre.roux@onera.fr
- PGP key : here or on pgp.mit.edu with fingerprint B00BA74D.
- ORCID:
https://orcid.org/0000-0003-2910-4738
Students
I am coadvising the PhD thesis of Lucien Rakotomalala with my colleague Marc Boyer on formal proofs of network calculus, funded by the RT-proofs ANR project.
Teaching
Validation par Analyse Statique : interprétation abstraite
Troisième année ENSEEIHT et master SRLC, enseigné en 2011-12 et 2013-14.
Transparents
- Cours 1/3
- Cours 2/3 (démo GCC : exemple.c)
- Cours 3/3 (démo flottants : flottants.c)
TP
- TP 1/3 (rappels sur les domaines abstraits et sur OCaml), correction
- TP 2/3 et 3/3, correction
Analyseur pour les TP
Software
- OSDP is an OCaml library offering interface to a few Semi-Definite Programming (SDP) solvers. Its main particularity lies in its ability to return verified results (against numerical errors).
- ValidSDP is mostly a Coq implementation of the above, enabling to automatically and efficiently prove that polynomials are positive (under polynomial constraints).
- Alt-Ergo OSDP is a OSDP plugin to the Alt-Ergo theorem prover, enabling it to verify some polynomial goals.
- RINY is a prototype static analyzer using the OSDP library.
- acsl.el: an Emacs mode for the C specification language ACSL used in tool Frama-C. It is an extension to Emac's C mode bringing mostly syntactic coloration of ACSL's special comments and a basic automatic indentation of those. Please note that this file is now distributed with Frama-C probably making this version obsolete.
- evmdd-smc: a symbolic model checker written during my first year of master internship (internship report).
- I also contribute to softwares such as Coq or its libraries Flocq for floating-point formalization or paramcoq to help refinement proofs.
Publications
- Primitive Floats in Coq,
Guillaume Bertholon, Érik Martin-Dorel, Pierre Roux,
ITP 2019, Portland, Septembre 2019 (pdf, slides) - A Non-linear Arithmetic Procedure for Control-Command Software Verification,
Pierre Roux, Mohamed Iguernlala, Sylvain Conchon,
TACAS 2018, Thessaloniki, Avril 2018 (pdf, slides) - Validating Numerical Semidefinite Programming Solvers for Polynomial Invariants (extended version of SAS 2016),
Pierre Roux, Yuen-Lam Voronin, Sriram Sankaranarayanan,
Formal Methods in System Design, 2018 (pdf) - Preserving Functional Correctness of Cyber-Physical System Controllers: From Model to Code,
Guillaume Davy, Christophe Garion, Pierre-Loïc Garoche, Pierre Roux, Xavier Thirioux,
FDL 2018, Munich, Novembre 2018 - A reflexive tactic for polynomial positivity using numerical solvers and floating-point computations,
Érik Martin-Dorel, Pierre Roux,
CPP 2017, Paris, Janvier 2017 (pdf, slides, BibTex) - Formal Proofs of Rounding Error Bounds - With Application to an Automatic Positive Definiteness Check,
Pierre Roux,
Journal of Automated Reasoning, 57(2): 135-156, 2016 (pdf, BibTex) - Embedding network calculus and event stream theory in a common model,
Marc Boyer, Pierre Roux,
ETFA 2016, Berlin, September 2016 (pdf, slides (by Marc Boyer), BibTex) - Validating Numerical Semidefinite Programming Solvers for Polynomial Invariants,
Pierre Roux, Yuen-Lam Voronin, Sriram Sankaranarayanan,
SAS 2016, Edinburgh, September 2016 (pdf, slides, BibTex) - Formal Analysis of Robustness at Model and Code Level,
Timothy E. Wang, Pierre-Loïc Garoche, Pierre Roux, Romain Jobredeaux, Eric Feron,
HSCC 2016, Vienna, April 2016 (pdf, slides (by Pierre-Loïc Garoche), BibTex) - Practical Policy Iterations,
Pierre Roux, Pierre-Loïc Garoche,
Formal Methods in System Design, 46(2): 163-196, 2015 (pdf, BibTex) - Closed Loop Analysis of Control Command Software,
Pierre Roux, Romain Jobredeaux, Pierre-Loïc Garoche,
HSCC 2015, Seattle, April 2015 (pdf, BibTex) - Innocuous Double Rounding of Basic Arithmetic Operations,
Pierre Roux,
Journal of Formalized Reasoning, 7(1): 131-142, May 2014 (pdf, BibTex) - Computing Quadratic Invariants with Min- and Max-Policy Iterations: a Practical Comparison,
Pierre Roux, Pierre-Loïc Garoche,
FM 2014, Singapour, May 2014 (pdf, BibTex) - Analyse statique de systèmes de contrôle commande : synthèse d’invariants non linéaire,
Pierre Roux,
PhD thesis, ISAE, December 2013 (pdf, slides, benchmarks) - Integrating Policy Iterations in Abstract Interpreters,
Pierre Roux, Pierre-Loïc Garoche,
ATVA 2013, Hanoï, October 2013 (pdf, slides, BibTex) - Formal Methods for the Analysis of Critical Control Systems Models: Combining Non-Linear and Linear Analyses,
Adrien Champion, Rémi Delmas, Michael Dierkes, Pierre-Loïc Garoche, Romain Jobredeaux, Pierre Roux,
FMICS 2013, Madrid, September 2013 (pdf, slides (by Pierre-Loïc Garoche), BibTex) - Formal Methods for the Analysis of Critical Control Systems Models: Combining Non-Linear and Linear Analyses,
Adrien Champion, Rémi Delmas, Michael Dierkes, Pierre-Loïc Garoche, Romain Jobredeaux, Pierre Roux,
SAE Aerotech 2013, Montreal, September 2013 - A Polynomial Template Abstract Domain based on Bernstein Polynomials,
Pierre Roux, Pierre-Loïc Garoche,
NSV 2013, Philadelphia, April 2013 (pdf, slides, BibTex) - A Generic Ellipsoid Abstract Domain for Linear Time Invariant Systems,
Pierre Roux, Romain Jobredeaux, Pierre-Loïc Garoche, Éric Féron,
HSCC 2012, Beijing, April 2012 (pdf, slides, BibTex) - Towards Cooperation of Formal Methods for the Analysis of Critical Control Systems (Arch T. Colwell Merit Award),
Adrien Champion, Rémi Delmas, Pierre-Loïc Garoche, Pierre Roux,
SAE International Journal of Aerospace, 4(2):850-858, 2011 (DOI, BibTex) - Dessine moi un domaine abstrait fini - une recette à base de Camlp4 et de solveurs SMT,
Pierre Roux, Pierre Loïc Garoche,
JFLA 2011, La Bresse, February 2011 (pdf, slides, BibTex) - SMT-AI: an Abstract Interpreter as Oracle for k-induction,
Pierre Roux, Rémi Delmas, Pierre-Loïc Garoche,
TAPAS'10 (Workshop of SAS 2010), Perpignan, September 2010 (pdf, slides, BibTex) - Model Checking with Edge-valued Decision Diagrams (short paper),
Pierre Roux, Radu Siminiceanu,
NASA Formal Methods Symposium (NFM 2010), Washington, DC, April 2010 (pdf, slides, BibTex)
Misc
I occasionally fold (origami): a few (old) images.
