Comment faire confiance à un compilateur?

Comment faire confiance a` un compilateur?Xavier LeroyINRIA Paris RocquencourtColloquium J. Morgenstern, 2009 10 08X. Leroy (INRIA) Ver´ ifier un compilateur 2009 10 08 1 / 51Contexte : les methodes´ formelleset la ver´ ification de programmesX. Leroy (INRIA) Ver´ ifier un compilateur 2009 10 08 2 / 51Le bug«En informatique, il y a le bug; c’est comme c¸a, vous n’y pouvez rien.»(Ger´ ard Berry, College` de France, 17/01/2008.)Toler´ able? Intoler´ able!X. Leroy (INRIA) Ver´ ifier un compilateur 2009 10 08 3 / 51Le logiciel critiqueLes methodes´ classiques :´ ´ ˆMethodologie de developpement extremement rigoureuse.Des tests, des tests, et encore des tests.Lorsque tout cela ne suffit plus ou couteˆ trop cher :les methodes´ formelles (approches mathematiques)´X. Leroy (INRIA) Ver´ ifier un compilateur 2009 10 08 4 / 51Ver´ ification sur un modele`Specifications´Model checkingPreuve manuelle`Modele(simplifie)´?ProgrammesourceX. Leroy (INRIA) Ver´ ifier un compilateur 2009 10 08 5 / 51Ver´ ification sur un modele`Specifications´Model checkingPreuve manuelle`Modele(simplifie)´?ProgrammesourceX. Leroy (INRIA) Ver´ ifier un compilateur 2009 10 08 5 / 51Ver´ ification formelle de programmesSpecifications´Model checkingPreuve manuelleAnalyse statique`Modele(simplifie)´Preuve de programme?ProgrammesourceX. Leroy (INRIA) Ver´ ifier un compilateur 2009 10 08 6 / 51L’analyse statique pour la suretˆ e´´Etablir automatiquement des propriet´ es´ de ...