Nous contacter

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.
  • ORCID: https://orcid.org/0000-0003-2910-4738

Students

I coadvised the PhD thesis of Lucien Rakotomalala with my colleague Marc Boyer on formal proofs of network calculus, funded by the RT-proofs ANR project (defended in February 2022).I also coadvised the PhD thesis of Baptiste Pollien with my colleagues Xavier Thirioux and Christophe Garion from ISAE and Gautier Hattenberger from ENAC on the verification of the Paparazzi drone autopilot (defended in November 2023).

Teaching

I regularly teach functional programming (with OCaml), bases of proof-assitants (with Coq) or bases of process algebras.

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

  • I'm a developer of Coq and its mathematical library MathComp. I also maintain or sometime contribute to other Coq libraries such as Flocq for floating-point formalization or paramcoq to help refinement proofs.
  • ValidSDP is mostly a Coq implementation of the above, enabling to automatically and efficiently prove that polynomials are positive (under polynomial constraints).
  • 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).
  • 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).

Publications

  • Enabling Floating-Point Arithmetic in the Coq Proof Assistant,
    Érik Martin-Dorel, Guillaume Melquiond, Pierre Roux,
    JAR, 2023 (pdf, BibTex)
  • CTA: A Correlation-Tolerant Analysis of the Deadline-Failure Probability of Dependent Tasks,
    Filip Markovic, Pierre Roux, Sergey Bozhko, Alessandro V. Papadopoulos, Björn B. Brandenburg,
    RTSS 2023, Taipei, December 2023 (pdf, BibTex)
  • A Verified UAV Flight Plan Generator,
    Baptiste Pollien, Christophe Garion, Gautier Hattenberger, Pierre Roux, Xavier Thirioux,
    FormaliSE 2023, Melbourne, May 2023 (pdf, BibTex)
  • A Formal Link Between Response Time Analysis and Network Calculus,
    Pierre Roux, Sophie Quinton, Marc Boyer,
    ECRTS 2022, Modena, July 2022 (pdf, BibTex)
  • A Residual Service Curve of Rate-Latency Server Used by Sporadic Flows Computable in Quadratic Time for Network Calculus,
    Marc Boyer, Pierre Roux, Hugo Daigmorte, David Puechmaille,
    ECRTS 2021, online, July 2021 (pdf, BibTex)
  • Verifying the Mathematical Library of an UAV Autopilot with Frama-C,
    Baptiste Pollien, Christophe Garion, Gautier Hattenberger, Pierre Roux, Xavier Thirioux,
    FMICS 2021, Paris, August 2021 (pdf, BibTex)
  • Verifying Min-Plus Computations with Coq,
    Lucien Rakotomalala, Pierre Roux, Marc Boyer,
    NFM 2021, online, May 2021 (pdf, BibTex)
  • 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.