Verified squared: does critical software deserve verified tools?

Xavier Leroy 1, *
* Auteur correspondant
Abstract : The formal verification of programs have progressed tremendously in the last decade. Principled but once academic approaches such as Hoare logic and abstract interpretation finally gave birth to quality verification tools, operating over source code (and not just idealized models thereof) and able to verify complex real-world applications. In this talk, I review some of the obstacles that remain to be lifted before source-level verification tools can be taken really seriously in the critical software industry: not just as sophisticated bug-finders, but as elements of absolute confidence in the correctness of a critical application.
Type de document :
Communication dans un congrès
POPL 2011 - 38th symposium Principles of Programming Languages, Jan 2011, Austin, United States. ACM, pp.1-2, 〈10.1145/1926385.1926387〉
Liste complète des métadonnées

Littérature citée [18 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01076682
Contributeur : Xavier Leroy <>
Soumis le : mercredi 22 octobre 2014 - 18:16:52
Dernière modification le : mercredi 29 juillet 2015 - 01:26:43
Document(s) archivé(s) le : vendredi 23 janvier 2015 - 11:20:42

Fichier

popl11-invited-talk.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Xavier Leroy. Verified squared: does critical software deserve verified tools?. POPL 2011 - 38th symposium Principles of Programming Languages, Jan 2011, Austin, United States. ACM, pp.1-2, 〈10.1145/1926385.1926387〉. 〈hal-01076682〉

Partager

Métriques

Consultations de la notice

91

Téléchargements de fichiers

108