Les erreurs logiciel peuvent avoir des conséquences désastreuses, causant des morts, des pertes financières considérables… Dans cette situation, nous voulons prouver que le code est correct : il ne plante pas, il fait ce qu’on attend de lui, il ne fuite pas d’information sensible… L’interprétation abstraite nous offre une façon de prouver de telles propriétés en utilisant une surapproximation de la sémantique. Notre cas d’étude est un système d’exploitation d’une plateforme d’accueil dans les avions, qui se situe à la frontière entre le monde de confiance, et le reste du monde, potentiellement hostile. Par conséquent, nous voulons prouver que le code non sûr ne peut pas perturber le code de confiance. Pour cela, nous devons étendre l’analyseur C que nous développons comme le code de l’OS contient des blocs d’assembleur x86 inline dans le code C. De plus, les propriétés que nous voulons prouver ne sont pas expressibles en C: on a besoin d’une sémantique plus précise de l’assembleur.