Colloquium d'informatique

2012-2013 - Campus Jussieu

Séminaire de prestige en recherche informatique. Invitation de grands noms du domaine, visant un public large.

Desperately seeking software perfection

Envie d'utiliser un autre lecteur ? (VLC, Quicktime, ...) Cliquez ici.
Envie de télécharger cette vidéo sur votre ordinateur ?Cliquez ici.
Signaler un problème avec la vidéo.

Résumé

In the general public, "software" has become synonymous with "bugs" and "security holes". Yet, there exists life-critical software systems that achieve extraordinary levels of reliability, as I'll illustrate with fly-by-wire systems in airplanes. A recent development in this area is the introduction of tool-assisted formal verification (static analysis and program proof) to complement, and sometimes replace, traditional test-based verification. However, the assurance provided by formal verification is limited by the confidence we can have in the verification tools and in the compilers that produce actual executables from verified sources. Using the CompCert verified C compiler as an example, I'll show the effectiveness of formally verifying, with the help of proof assistants, the tools that participate in the construction and verification of critical software.


Orateur(s) : Xavier Leroy, INRIA
Public : Tous
Date : Mardi 20 Octobre 2015 18:00
Lieu : Amphithéâtre 25 site jussieu