La vérification des programmes par interprétation abstraite