Preservation of proof obligations for hybrid verification methods

Gilles Barthe 1 César Kunz 2 David Pichardie 3 Julian Samborski-Forlese 1
2 EVEREST - Environments for Verification and Security of Software
CRISAM - Inria Sophia Antipolis - Méditerranée
3 Lande - Logiciel : ANalyse et DEveloppement
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires, Inria Rennes – Bretagne Atlantique
Abstract : Program verification environments increasingly rely on hybrid methods that combine static analyses and verification condition generation. While such verification environments operate on source programs, it is often preferable to achieve guarantees about executable code. We show that, for a hybrid verification method based on numerical static analysis and verification condition generation, compilation preserves proof obligations and therefore it is possible to transfer evidence from source to compiled programs. Our result relies on the preservation of the solutions of analysis by compilation; this is achieved by relying on a bytecode analysis that performs symbolic execution of stack expressions in order to overcome the loss of precision incurred by performing static analyses on compiled (rather than source) code. Finally, we show that hybrid verification methods are sound by proving that every program provable by hybrid methods is also provable (at a higher cost) by standard methods.
Type de document :
Communication dans un congrès
6th IEEE International Conferences on Software Engineering and Formal Methods (SEFM'08), 2008, Cape Town, South Africa. 2008
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00332718
Contributeur : David Pichardie <>
Soumis le : mardi 21 octobre 2008 - 15:20:01
Dernière modification le : mercredi 16 mai 2018 - 11:23:03
Document(s) archivé(s) le : mardi 9 octobre 2012 - 14:06:18

Fichier

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00332718, version 1

Collections

Citation

Gilles Barthe, César Kunz, David Pichardie, Julian Samborski-Forlese. Preservation of proof obligations for hybrid verification methods. 6th IEEE International Conferences on Software Engineering and Formal Methods (SEFM'08), 2008, Cape Town, South Africa. 2008. 〈inria-00332718〉

Partager

Métriques

Consultations de la notice

204

Téléchargements de fichiers

67