Si la production de logiciel fiable est depuis longtemps la préoccupation d'ingénieurs, elle devient à ce jour une branche de sujets de recherche riche en applications, dont l'analyse statique. Ce travail a porté sur l'analyse statique de programmes et, plus précisément, sur l'analyse des propriétés numériques. Ces analyses sont traditionnellement basées sur le concept de domaine abstrait. Le problème est que, ce n'est pas évident d'étendre ces domaines dans le contexte de programmes avec pointeurs. Nous avons proposé une approche qui sait systématiquement combiner ces domaines avec l'information de l'analyse de points-to (une sorte d'analyse de pointeurs). L'approche est formalisée en théorie de l'interprétation abstraite, prouvée correct et prototypée avec une modular implémentation qui sait inférer des propriétés numériques des programmes de millions de lignes de codes. La deuxième partie de la thèse vise à améliorer la précision de l'analyse points-to. Nous avons découvert que l'analyse de must-alias (qui analyse si deux variables sont nécessairement égaux) peut servir à raffiner l'analyse points-to. Nous avons formalisé cette combinaison en s'appuyant sur la notion de bisimulation, bien connue en vérification de modèle ou théorie de jeu... Un algorithme de complexité quadruple est proposé et prouvé correct.