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.
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.
One particularly popular moment associated to the colloquium is the “Master Class” where students have the opportunity to give a short (but well-prepared) presentation of his/her work. Each presentation (10 minutes) is followed by an open discussion with the guest speaker (15 minutes) who gives a detailed feedback. The complete program is provided here.
Launched in 2012, the Colloquium d’Informatique de Sorbonne Université is a recurring event that invites major figures of the computer science field to give special lectures on the campus of Sorbonne University’s Science and Engineering Faculty. It targets a diverse yet technically-informed audience, and especially computer science researchers from all specialities, PhD students, and computer science students at master level.
The Colloquium’s main event is the invited speaker’s lecture, a 45-minute talk followed by questions and interactions with the audience. Generally, this lecture is associated with a masterclass reserved for PhD students from LIP6 and/or other labs.
As the main driving force behind to the steering committee, LIP6 oversees the Colloquium’s organisation, with occasional support from ISIR.