Skip to Main content Skip to Navigation
Conference papers

In Search of Software Perfection: An introduction to deductive software verification

Abstract : 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 invited talk discussed the usability of these tools, based on examples in Frama-C WP and in Coq, and speculated on what is next on the road to software perfection.
Complete list of metadata

https://hal.inria.fr/hal-02392114
Contributor : Xavier Leroy Connect in order to contact the contributor
Submitted on : Tuesday, December 3, 2019 - 6:54:08 PM
Last modification on : Wednesday, June 30, 2021 - 3:35:36 AM

Identifiers

  • HAL Id : hal-02392114, version 1

Collections

CDF | PSL

Citation

Xavier Leroy. In Search of Software Perfection: An introduction to deductive software verification. BOB Summer 2019 Konferenz, Aug 2019, Berlin, Germany. ⟨hal-02392114⟩

Share

Metrics

Record views

70