Colloquium with professor Xavier Leroy

Abstract

In June 1949, in a workshop communication titled "Checking a large routine" that would not be published until 1984, Alan Turing outlined an approach to prove correctness properties of programs with mathematical certainty. This approach, known today as deductive software verification, was reinvented and expanded by Floyd in 1967, put on solid logical ground by Hoare in 1969, studied extensively throughout the 1970s, nearly abandoned and replaced by more automated verification techniques in the 1980s and 1990s, and revived in the 2000s thanks to advances in automated deduction. 

After providing an overview of this tumultuous history, I will show how deductive verification is being reinvented again, with less emphasis on automation and more emphasis on proof engineering, as part of a general movement toward mechanised mathematics using proof assistants.

Speaker's bio

Xavier Leroy is a professor of software sciences at Collège de France in Paris and a member of the French Academy of Sciences.  His research interests include programming languages and systems, and the formal verification of software for safety and security. He is the architect and original developer of the OCaml programming language and its implementation, one of the most widely used typed functional programming languages. His current work focuses on the formal verification of programming languages and tools, and especially on the CompCert verified C compiler, the first realistic compiler that has been mathematically proved correct.

Sign up via the Choodle link to get a sandwich. Deadline 30 september.