I’ll defend my habilitation thesis on December 1st at 9:30 CET=UTC+1. Rocq took an important role in that work. I’ll put a sharing link on my webpage
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. Toulouse INP (examiner)