La vérification déductive de logiciels : comment démontrer des théorèmes à propos d'un programme ?

Conférence de Xavier Leroy, Professeur, chaire de sciences du logiciel - Collège de France, Paris

11H salle Marcel Pierre à Palaiseau

Dès 1949, Alan Turing invente une approche qui permet de raisonner mathématiquement sur toutes les exécutions possibles d'un programme.  En 1968, C.A.R. Hoare met en évidence une logique de programmes qui sous-tend et valide de tels raisonnements.  C'est la naissance de la vérification déductive des logiciels, aussi appelée «preuve de programmes», une alternative au test qui permet de vérifier qu'un programme fait ce qu'il est censé faire et ne contient pas de «bugs» avec la certitude des mathématiques.

Longtemps considérée comme purement théorique et inapplicable en pratique, la vérification déductive est aujourd'hui beaucoup plus facile d'emploi, grâce à des outils d'analyse de logiciel comme Frama-C ou Infer, et commence à être utilisée dans l'industrie aéronautique.  Mon exposé introduira les principes de la vérification déductive de programmes et illustrera son utilisabilité pratique.

Télécharger le poster

Merci de vous inscrire auprès de fabienne.debruyere @ onera.fr au plus tard 4 jours avant la date de la conférence, en précisant en objet du mél « ASLConf - Accès » et en fournissant les informations suivantes : nom, prénom, date et lieu de naissance, société ou organisation, fonction, n° CNI ou n° passeport. Pour les ressortissants étrangers, y compris CE, faire cette démarche deux semaines à l'avance, en ajoutant un scan du passeport. Toute demande tardive ne pourra être traitée, et l’accès au site de l’ONERA ne sera donc pas garanti.

Pour recevoir les annonces des prochaines AeroSpace Lab conferences, abonnez vous à notre liste de diffusion en vous adressant à fabienne.debruyere @ onera.fr , avec l'objet "ASLConf - Annonces".

Accès

ONERA
6 chemin de la Vauve aux Granges , Palaiseau
Accéder au centre ONERA de Palaiseau

Calendrier des Aerospace Lab Conferences