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.

HDR

I defended my habilitation thesis (HDR) on Monday December 1st.

Abstract

Numerical Computations and Proofs: from Proof-Assistants to Aerospace Applications

Digital flight commands are pervasive in modern airliners, for a number of reason we'll quickly summarize. This software being critical, they demand a very high quality level, which is currently ensured through expansive (and expensive) testing. We'd like to develop formal methods to replace some of those tests by mathematical proofs.

At the core of flight commands lie numerical computations. In order to verify them, we investigated methods based on sum of squares (SOS) polynomials, using semidefinite programing (SDP). These numerical solvers efficiently produce approximate solutions, thanks to floating-point computations. Unfortunately, rounding errors can lead to unreliable results, sometimes without much clue indicating the result is wrong. We thus developed a method to derive rigorous proofs from such approximate solutions.

This method has been implemented as an automatic tactic in the proof assistant Rocq (formerly known as Coq). In order to enable efficient proofs based on numerical computations, this led us to develop some hardware floating-point support in Rocq.

Critical embedded systems also rely on network which need to fulfill some real-time constraints. Multiple technologies are available, among which rate constrained networks, using network calculus to ensure the real-time constraints are met. We formalized within Rocq both theoretical network-calculus results and the tropical-algebra computations required by actual analyses.

We'll end the presentation with a quick overview of more technical activities : contributions to the Rocq proof-assistant and its MathComp library, as well as an example of technical expertise on the embedded network of the Ariane 6 launcher.

Keywords:

digital flight commands, embedded systems, formal methods, Sum of Squares (SOS) polynomials, convex optimization, semidefinite programming (SDP), proof assistants, Rocq, Coq, floating-point arithmetic, network calculus

Jury:

  • Andrew Appel, Emeritus prof. Princeton, visiting prof. Cornell (reviewer)
  • Assia Mahboubi, DR INRIA Nantes (reviewer)
  • David Monniaux, DR CNRS Grenoble (reviewer)
  • Yves Bertot, DR INRIA Nice (examiner)
  • Sylvie Boldo, DR INRIA Saclay (examiner)
  • Emmanuel Grolleau, Prof. ENSMA (examiner)
  • Didier Henrion, DR CNRS Toulouse (examiner)
  • Philippe Queinnec, Prof. INPT (examiner)

Contact

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 proved implementation of OSDP, 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

  • Formalizing Concentration Inequalities in Rocq: Infrastructure and Automation,
    Reynald Affeldt, Alessandro Bruni, Cyril Cohen, Pierre Roux, Takafumi Saikawa,
    ITP, 2025 (pdf, BibTex)
  • 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, benchmarks)
  • 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, tool, benchmarks)
  • 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.