BOB Summer 2019 - Xavier Leroy, In Search of Software Perfection
Channel: BOB
Date: 2019-09-02

Xavier Leroy,
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.

https://bobkonf.de/2019-summer/leroy.html