Result Certification of Static Program Analysers with Automated Theorem Provers

Frédéric Besson 1 Pierre-Emmanuel Cornilleau 1 Thomas Jensen 1
1 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : The automation of the deductive approach to program veri- fication crucially depends on the ability to efficiently infer and discharge program invariants. In an ideal world, user-provided invariants would be strengthened by incorporating the result of static analysers as untrusted annotations and discharged by automated theorem provers. However, the results of object-oriented analyses are heavily quantified and cannot be discharged, within reasonable time limits, by state-of-the-art auto- mated theorem provers. In the present work, we investigate an original approach for verifying automatically and efficiently the result of certain classes of object-oriented static analyses using off-the-shelf automated theorem provers. We propose to generate verification conditions that are generic enough to capture, not a single, but a family of analyses which encompasses Java bytecode verification and Fähndrich and Leino type- system for checking null pointers. For those analyses, we show how to generate tractable verification conditions that are still quantified but fall in a decidable logic fragment that is reducible to the Effectively Propositional logic. Our experiments confirm that such verification conditions are efficiently discharged by off-the-shelf automated theorem provers.
Type de document :
Communication dans un congrès
VSTTE 2013 - Fifth Working Conference on Verified Software: Theories, Tools and Experiments, 2013, Atherthon, United States. 2013
Liste complète des métadonnées

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

https://hal.inria.fr/hal-00924167
Contributeur : Frédéric Besson <>
Soumis le : lundi 6 janvier 2014 - 14:37:17
Dernière modification le : vendredi 16 novembre 2018 - 01:37:45
Document(s) archivé(s) le : jeudi 10 avril 2014 - 16:45:35

Fichier

result_certification_of_static...
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00924167, version 1

Citation

Frédéric Besson, Pierre-Emmanuel Cornilleau, Thomas Jensen. Result Certification of Static Program Analysers with Automated Theorem Provers. VSTTE 2013 - Fifth Working Conference on Verified Software: Theories, Tools and Experiments, 2013, Atherthon, United States. 2013. 〈hal-00924167〉

Partager

Métriques

Consultations de la notice

2413

Téléchargements de fichiers

247