L'interprétation abstraite est une théorie décrivant comment calculer automatiquement des propriétés sur des programmes. Elle est notamment utilisée pour prouver l'absence de certaines erreurs dans des logiciels de grande taille, dans des contextes industriels variés allant des applications .NET aux codes embarqués critiques de l'aéronautique. Par exemple, l'interprétation abstraite a été utilisée pour démontrer des propriétés sur des programmes dans des domaines aussi divers que les systèmes concurrents, les protocoles de communication, le calcul de pires temps d'exécution, ou encore l'adressage mémoire. Dans un premier temps, ce chapitre propose une introduction à l'interprétation abstraite. Nous présenterons les concepts fondamentaux de cette théorie : calcul de propriétés et notion de domaine abstrait, correspondance entre les sémantiques concrètes et abstraites, calcul efficace de point fixe dans l'abstrait. Ensuite, nous illustrerons ces notions par l'utilisation de domaines pour la qualité numérique et pour la détection des sources d'imprécision des calculs en nombres flottants.
