Thèse Maitriser la Transition des Nombres Mathématiques et leurs Implementations dans les Ordinateurs H/F - Université Paris-Saclay GS Informatique et sciences du numérique

Établissement : Université Paris-Saclay GS Informatique et sciences du numérique
École doctorale : Sciences et Technologies de l'Information et de la Communication
Laboratoire de recherche : Laboratoire Méthodes Formelles
Direction de la thèse : Burkhart WOLFF ORCID 0000000296487663
Début de la thèse : 2026-10-01
Date limite de candidature : 2026-03-22T23:59:59

PROFIL ET COMPETENCES REQUIS

Nous recherchons un(e) doctorant(e) enthousiaste possédant une solide formation en informatique, génie logiciel, mathématiques ou dans un domaine étroitement lié. Une expertise en méthodes formelles - telles que le raisonnement sur les programmes, la sémantique des langages de programmation, la vérification de modèles, la démonstration de théorèmes ou
la logique algorithmique - est essentielle.

CONTEXT

Les modèles mathématiques, par exemple ceux qui décrivent des systèmes physiques ou des algorithmes cryptographiques, reposent sur des nombres idéaux. Par exemple, les entiers mathématiques sont infinis et les nombres réels mathématiques sont continus et infinis. Les ordinateurs fonctionnent avec des approximations finies, bornées (c'est-à-dire qu'il existe un plus petit et un plus grand nombre) et discrètes. Ce «fossé numérique» entre les modèles mathématiques et les systèmes réels représente un défi lors de la mise en oeuvre de systèmes critiques pour la sécurité: par exemple, les avions autonomes ou les voitures autonomes nécessitent des représentations de haute précision de leur position pour éviter les collisions. Par conséquent, ne pas tenir compte de l'approximation de la représentation approximative des nombres dans les ordinateurs peut entraîner des accidents susceptibles de mettre en danger des vies humaines. De plus, de nombreux systèmes critiques pour la sécurité, et pas seulement les algorithmes cryptographiques, reposent sur une gestion correcte des dépassements de capacité (overflow et underflow) dans les calculs sur les entiers. En effet, les bogues liés aux dépassements de capacité sont à l'origine d'un grand nombre de vulnérabilités exploitées par les cybercriminels, notamment pour le vol de cryptomonnaies d'une valeur de plusieurs milliards de dollars. Bien que ce problème ne soit pas nouveau (par exemple, dès 1982, une erreur de conversion de nombres à virgule flottante dans un système de négociation de la Bourse de Vancouver a entraîné une perte de
plusieurs millions de dollars américains), aucune méthode de développement intégrée permettant de prévenir de tels bogues n'est encore disponible.

OBJECTIFS

Ce projet de doctorat vise à relever ce défi en développant une approche rigoureuse pour la conception de systèmes reposant sur des représentations précises des nombres, à l'aide du démonstrateur de théorèmes interactif
Isabelle/HOL. Le projet de doctorat peut porter sur:

1) la formalisation de représentations concrètes des nombres machine (par exemple, IEEE 754, POSIT, nombres décimaux à virgule flottante, arithmétique à virgule fixe), leurs propriétés (algébriques) et leur relation avec les nombres mathématiques abstraits;

2) la formalisation et la vérification d'algorithmes numériques ou cryptographiques, avec la création d'une bibliothèque réutilisable et vérifiée;

3) la formalisation et la vérification de la théorie et des algorithmes de la géométrie algorithmique (voir [9]);

4) le développement d'une approche de raffinement de bout en bout, des modèles mathématiques aux représentations machine.

La thèse sera co-dirigée par le Professeur Achim Brucker (****@****.**) et le Professeur Burkhart Wolff (****@****.**), et mènera à un double diplôme de l'Université d'Exeter et de l'Université Paris-Saclay.

PLAN DE TRAVAIL (proposition A)

- Refondre la bibliothèque existante de raisonnement sur les nombres à virgule flottante dans Coq
- Développer plusieurs études de cas: algorithmes et leurs améliorations
- Élaborer une théorie des bornes d'erreur

PLAN DE TRAVAIL (proposition B)

- Développer une bibliothèque et un support pour l'arithmétique à virgule fixe
- Développer plusieurs algorithmes efficaces pour la résolution de problèmes de lignes, de trajectoires et de zonotopes
- Applications dans le domaine des stratégies de conduite sécuritaire

Les modèles mathématiques, par exemple ceux qui décrivent des systèmes physiques ou des algorithmes cryptographiques, reposent sur des nombres idéaux. Par exemple, les entiers mathématiques sont infinis et les nombres réels mathématiques sont continus et infinis. Les ordinateurs fonctionnent avec des approximations finies, bornées (c'est-à-dire qu'il existe un plus petit et un plus grand nombre) et discrètes. Ce «fossé numérique» entre les modèles mathématiques et les systèmes réels représente un défi lors de la mise en oeuvre de systèmes critiques pour la sécurité: par exemple, les avions autonomes ou les voitures autonomes nécessitent des représentations de haute précision de leur position pour éviter les collisions. Par conséquent, ne pas tenir compte de l'approximation de la représentation approximative des nombres dans les ordinateurs peut entraîner des accidents susceptibles de mettre en danger des vies humaines. De plus, de nombreux systèmes critiques pour la sécurité, et pas seulement les algorithmes cryptographiques, reposent sur une gestion correcte des dépassements de capacité (overflow et underflow) dans les calculs sur les entiers. En effet, les bogues liés aux dépassements de capacité sont à l'origine d'un grand nombre de vulnérabilités exploitées par les cybercriminels, notamment pour le vol de cryptomonnaies d'une valeur de plusieurs milliards de dollars. Bien que ce problème ne soit pas nouveau (par exemple, dès 1982, une erreur de conversion de nombres à virgule flottante dans un système de négociation de la Bourse de Vancouver a entraîné une perte de
plusieurs millions de dollars américains), aucune méthode de développement intégrée permettant de prévenir de tels bogues n'est encore disponible.

Ce projet de doctorat vise à relever ce défi en développant une approche rigoureuse pour la conception de systèmes reposant sur des représentations précises des nombres, à l'aide du démonstrateur de théorèmes interactif
Isabelle/HOL.

Preuve formelle des algorithmes par raffinement.

Motiv'e de travaille dans la domaine méthodes formelles avec des applications dans les algorithmes numériques (safety, security)