Certified Result Checking for Polyhedral Analysis of Bytecode Programs

Frédéric Besson 1 Thomas Jensen 1 David Pichardie 1 Tiphaine Turpin 1
1 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : Static analysers are becoming so complex that it is crucial to ascertain the soundness of their results in a provable way. In this paper we develop a certified checker in Coq that is able to certify the results of a polyhedral array-bound analysis for an imperative, stack-oriented bytecode language with procedures, arrays and global variables. The checker uses, in addition to the analysis result, certificates which at the same time improve efficiency and make correctness proofs much easier. In particular, our result certifier avoids complex polyhedral computations such as convex hulls and is using easily checkable inclusion certificates based on Farkas lemma. Benchmarks demonstrate that our approach is effective and produces certificates that can be efficiently checked not only by an extracted Caml checker but also directly in Coq.
Type de document :
Communication dans un congrès
The 5th International Symposium on Trustworthy Global Computing (TGC), 2010, Munich, Germany. Springer-Verlag, 2010, Lecture Notes in Computer Science
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00537816
Contributeur : David Pichardie <>
Soumis le : vendredi 19 novembre 2010 - 14:15:58
Dernière modification le : mercredi 16 mai 2018 - 11:23:28
Document(s) archivé(s) le : vendredi 26 octobre 2012 - 16:01:51

Fichier

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

Identifiants

  • HAL Id : inria-00537816, version 1

Citation

Frédéric Besson, Thomas Jensen, David Pichardie, Tiphaine Turpin. Certified Result Checking for Polyhedral Analysis of Bytecode Programs. The 5th International Symposium on Trustworthy Global Computing (TGC), 2010, Munich, Germany. Springer-Verlag, 2010, Lecture Notes in Computer Science. 〈inria-00537816〉

Partager

Métriques

Consultations de la notice

338

Téléchargements de fichiers

110