Skip to Main content Skip to Navigation
Conference papers

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

Xavier Leroy 1
1 Chaire Sciences du logiciel
CAMBIUM - Langages de programmation : systèmes de types, concurrence, preuve de programme
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 <>
Submitted on : Tuesday, December 3, 2019 - 6:54:08 PM
Last modification on : Saturday, May 22, 2021 - 3:36:40 AM

Identifiers

  • HAL Id : hal-02392114, version 1

Collections

CDF | PSL | INRIA

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

77