Pierre Roux

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.

Stage

Je propose un sujet de stage de Master pour le printemps-été 2018 sur la preuve formelle en calcul réseau (http://w3.onera.fr/stages/sites/w3.onera.fr.stages/files/dtis-2018-046.pdf). Possibilité de poursuite en thèse (financement assuré par le projet ANR RT-proofs). N'hésitez pas à me contacter si vous êtes intéressé.

Teaching

Validation par Analyse Statique : interprétation abstraite

Troisième année ENSEEIHT et master SRLC, enseigné en 2011-12 et 2013-14.

Transparents

TP

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).
  • 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).

Publications

  • 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, 2017 (pdf)
  • 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