ONERA-CERT, Toulouse, France, 27 mai 2003.
Après un tour d'horizon rapide des méthodes formelles (méthodes déductives, méthodes exhaustives (model-checking), analyse statique), nous discutons leur application aux preuves d'invariance, en particulier par analyse statique. Nous expliquons ensuite (très informellement) quelques idées formalisées par la théorie de l'interprétation abstraite, que nous illustrons sur la vérification d'absence d'erreurs à l'exécution. Nous introduisons ensuite la distinction entre analyseurs statiques généraux et spécialisés, en donnant des exemples, et expliquons comment ces derniers peuvent réussir à éviter toute fausse alarme avec un coût d'analyse faible pour une famille d'applications dont les spécificités peuvent être prises en compte dans le choix des abstractions génériques utilisées dans l'analyse statique. Nous terminons en donnant quelques thèmes actuels de recherche en interprétation abstraite puis des références bibliographiques.
\bibitem{Cousot03-CERT}
P{.} Cousot.
\newblock V\'erification de programmes par interpr\'etation abstraite.
\newblock ONERA-CERT, Toulouse, France, 27 mai 2003.
@unpublished{Cousot03-CERT,
author = {P{.} Cousot},
title = {V\'erification de programmes par interpr\'etation abstraite},
note = {ONERA-CERT, Toulouse, France, 27 mai 2003},
}