Annonce
Colloquium d'Informatique de l'UPMC Sorbonne Universités
23 Septembre 2015
Catégorie : Journée d étude
C'est avec plaisir que nous vous convions à assister au prochain exposé organisé dans le cadre du Colloquium d'informatique de l'UPMC Sorbonne Universités [http://www.lip6.fr/colloquium/] intitulé
Desperately seeking software perfection
et présenté par Xavier Leroy, Inria Paris.
Ce colloquium s'adresse à un public large, et est ouvert à tous les chercheurs et étudiants en informatique.
L'exposé aura lieu :
Mardi 20 Octobre 2015 à 18h
Amphithéâtre 25
Université Pierre et Marie Curie
4, place Jussieu (métro Jussieu)
75005 Paris
Pour s'y rendre :
http://www.upmc.fr/fr/universite/campus_et_sites/a_paris_et_en_idf/jussieu.html
Un cocktail est prévu à 17h15 en prélude à la conférence.
Abstract:
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.
Short bio:
Xavier Leroy is a senior research scientist at Inria Paris where he leads the Gallium research team. His research focuses on programming languages and tools, and on the formal verification of software using program proof and static analysis. He is the architect and one of the main developers of the OCaml functional programming language and of the CompCert formally-verified C compiler.