Abstract FR:

L'analyse sémantique des programmes consiste à déterminer automatiquement à la compilation des propriétés qu'ils vérifient lors de toute execution. Cette thèse est plus particulièrement consacrée aux propriétés de congruence des variables (ou des abstractions) numériques. Précisément, à partir d'un cadre algébrique commun, on définit tout d'abord l'analyse de congruence arithmétique sur les nombres entiers, qui généralise à la fois la parite et la propagation des constantes, qu'on generalise elle-même à l'inférence de systèmes d'équations linéaires de congruence. On generalise ensuite ces deux analyses aux nombres rationnels. Entre autres, ces analyses peuvent s'avérer utiles dans le cadre de la vectorisation automatique pour les premières, et pour les secondes afin d'optimiser la représentation des réels et limiter les erreurs d'arrondi dans les calculs. On termine par la présentation rapide d'extensions des précédentes analyses, d'analyses de congruence multiplicative et de techniques d'iterations décroissantes permettant d'améliorer les résultats des analyses en général.