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

ONERA, Palaiseau

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

11H salle Marcel Pierre à Palaiseau

Xavier LeroyDè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 « Aerospace Lab Conferences - Accès » (pour les ressortissants étrangers - CE et hors CE, nous prévenir 2 semaines à l’avance). Toute demande tardive ne pourra être traitée, et l’accès au site de l’ONERA ne sera donc pas garanti.

Accès

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

 

Calendrier des Aerospace Lab Conferences

 

Back to the list