Ph.D
Group : Verification of Algorithms, Languages and Systems

Formalizations of error analysis in numerical analysis and floating-point arithmetic

Starts on 01/10/2016
Advisor : BOLDO, Sylvie

Funding : Autre financement à préciser
Affiliation : Université Paris-Saclay
Laboratory : LRI -l'amphithéâtre du bâtiment 660 (Claude Shanno

Defended on 13/12/2019, committee :

Research activities :

Abstract :
This thesis consists of three contributions related to the Coq formalization of error analysis
in numerical analysis and floating-point arithmetic.

First, we have exhibited an algorithm computing the average of two decimal floating-point numbers
and have proved that this algorithm computes the correct rounding. We have formalized the algorithm
and its correctness proof in the Coq proof assistant.

The second contribution of the thesis is the analysis and the formalization of rounding error bounds associated to the implementation of Runge-Kutta methods applied to linear systems. We have proposed a generic methodology to build a bound on the error accumulated over the iterations, taking potential underflow and overflow into account. We have then instantiated this methodology for classic Runge-Kutta methods, e.g. the Euler and RK2 methods. We have proposed a formalization of the results, including the definition of matrix norms, the proof of rounding error bounds for matrix operations and the formalization of the generic results and their instantiations.

Finally, we have proposed a formalization of functional analysis results that serve as foundations for the finite element method. This formalization is based on the Coquelicot library and includes the theory of Hilbert spaces, the formal proof of the Lax-Milgram Theorem and the proof of completeness of finite dimensional subspaces of Hilbert spaces.

CAUSAL LEARNING FOR DIAGNOSTIC SUPPORT


CAUSAL UNCERTAINTY QUANTIFICATION UNDER PARTIAL KNOWLEDGE AND LOW DATA REGIMES


MICRO VISUALIZATIONS: DESIGN AND ANALYSIS OF VISUALIZATIONS FOR SMALL DISPLAY SPACES
The topic of this habilitation is the study of very small data visualizations, micro visualizations, in display contexts that can only dedicate minimal rendering space for data representations. For several years, together with my collaborators, I have been studying human perception, interaction, and analysis with micro visualizations in multiple contexts. In this document I bring together three of my research streams related to micro visualizations: data glyphs, where my joint research focused on studying the perception of small-multiple micro visualizations, word-scale visualizations, where my joint research focused on small visualizations embedded in text-documents, and small mobile data visualizations for smartwatches or fitness trackers. I consider these types of small visualizations together under the umbrella term ``micro visualizations.'' Micro visualizations are useful in multiple visualization contexts and I have been working towards a better understanding of the complexities involved in designing and using micro visualizations. Here, I define the term micro visualization, summarize my own and other past research and design guidelines and outline several design spaces for different types of micro visualizations based on some of the work I was involved in since my PhD.