Depuis une vingtaine d'années, la résolution de problèmes d'optimisation globale non convexes avec contraintes a connu un formidable essor. Les algorithmes de branch and bound basée sur l'analyse d'intervalles ont su trouver leur place, car ils ont l'avantage de prouver l'optimalité de la solution de façon déterministe, avec un niveau de certitude pouvant aller jusqu'à la précision machine. Cependant, la complexité exponentielle en temps et en mémoire de ces algorithmes induit une limite intrinsèque, c'est pourquoi il est toujours nécessaire d'améliorer les techniques actuelles. - Dans cette thèse, nous avons développé de nouvelles arithmétiques basées sur l'arithmétique d'intervalles et l'arithmétique affine, afin de calculer des minorants et des majorants de meilleure qualité de fonctions explicites sur un intervalle. - Nous avons ensuite développé une nouvelle méthode automatique de construction de relaxations linéaires. Cette construction est basée sur l'arithmétique affine et procède par surcharge des opérateurs. Les programmes linéaires ainsi générés ont exactement le même nombre de variables et de contraintes d'inégalité que les problèmes originaux, les contraintes d'égalité étant remplacées par deux inégalités. Cette nouvelle procédure permet de calculer des minorants fiables et des certificats d'infaisabilité pour chaque sous-domaine à chaque itération de notre algorithme de branch and bound par intervalles. De nombreux tests numériques issus du site COCONUT viennent confirmer l'efficacité de cette approche. - Un autre aspect de cette thèse a été l'étude d'une extension de ce type d'algorithmes en introduisant une limite sur mémoire disponible. L'idée principale de cette approche est de proposer un processus inverse de l'optimisation par le biais d'un principe métaheuristique: plutôt que d'améliorer des solutions locales à l'aide de métaheuristiques telles que les algorithmes Taboo ou VNS, nous partons d'une méthode exacte et nous la modifions en une heuristique. De cette façon, la qualité de la solution trouvée peut être évaluée. Une étude de la complexité de ce principe métaheuristique a également été effectuée. - Enfin, pour finir l'étude, nous avons appliqué notre algorithme à la résolution de problème en géométrie plane, ainsi qu'à la résolution d'un problème de dimensionnement de moteur électrique. Les résultats obtenus ont permis de confirmer l'intérêt de ce type d'algorithme, en résolvant des problèmes ouverts sur les polygones convexes et proposant des structures innovantes en génie électrique.

Cette thèse s'articule autour de la formalisation de mathématiques dans l'assistant à la preuve Coq dans le but de vérifier des méthodes numériques. Plus précisément, elle se concentre sur la formalisation de concepts qui apparaissent dans la résolution des systèmes d'équations linéaires et non-linéaires. <p> Dans ce cadre, on a analysé la méthode de Newton, couramment utilisée pour approcher les solutions d'une équation ou d'un système d'équations. Le but a été de formaliser le théorème de Kantorovitch qui montre la convergence de la méthode de Newton vers une solution, l'unicité de la solution dans un voisinage, la vitesse de convergence et la stabilité locale de la méthode. L'étude de ce théorème a nécessité la formalisation de concepts d'analyse multivariée. En se basant sur ces résultats classiques sur la méthode de Newton, on a montré qu'arrondir à chaque étape préserve la convergence de la méthode, avec une corrélation bien déterminée entre la précision des données d'entrée et celle du résultat. Dans un travail commun avec Nicolas Julien nous avons aussi formellement étudié les calculs avec la méthode de Newton effectués dans le cadre d'une bibliothèque d'arithmétique réelle exacte. <p> Pour les systèmes linéaires d'équations, on s'est intéressé aux systèmes qui ont une matrice associée à coefficients intervalles. Pour résoudre de tels systèmes, un problème important qui se pose est de savoir si la matrice associée est régulière. On a fourni la vérification formelle d'une collection de critères de régularité pour les matrices d'intervalles.