Talk: (English)
In Search of Software Perfection
How to prove the correctness of a program with mathematical certainty? The principles of program proof have been known for a very long time, but it is only recently that program provers and proof assistants became able to verify nontrivial programs. This talk will discuss the usability of these tools, based on examples in Frama-C WP and in Coq, and speculate on what is next on the road to software perfection.
Xavier Leroy
Xavier Leroy is a senior scientist at INRIA interested in the scientific aspects of programming. He leads the Gallium team on the design, formalization, and implementation of programming languages and systems. He is well known for being the primary developer of the OCaml programming language and compiler.
- Slides
- xavier-leroy.pdf
