Vérification de propriétés LTL sur des programmes C par génération d'annotations

Nicolas Stouls 1 Julien Groslambert 2
1 AMAZONES - Ambient Middleware Architectures: Service-Oriented, Networked, Efficient and Secured
Inria Grenoble - Rhône-Alpes, CITI - CITI Centre of Innovation in Telecommunications and Integration of services
Résumé : Ce travail propose une méthode de vérification de propriétés temporelles basée sur la génération automatique d'annotations de programmes. Les annotations générées sont ensuite vérifiées par des prouveurs automatiques via un calcul de plus faible précondition. Notre contribution vise à optimiser une technique existante de génération d'annotations, afin d'améliorer l'automatisation de la vérification des obligations de preuve produites. Cette approche a été outillée sous la forme d'un plugin au sein de l'outil Frama-C pour la vérification de programmes~C
Type de document :
Rapport
[Rapport de recherche] 2011, pp.16
Liste complète des métadonnées

https://hal.inria.fr/inria-00568947
Contributeur : Nicolas Stouls <>
Soumis le : jeudi 24 février 2011 - 07:55:19
Dernière modification le : samedi 17 septembre 2016 - 01:32:26
Document(s) archivé(s) le : mercredi 25 mai 2011 - 02:37:36

Fichiers

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

Identifiants

  • HAL Id : inria-00568947, version 1

Collections

Citation

Nicolas Stouls, Julien Groslambert. Vérification de propriétés LTL sur des programmes C par génération d'annotations. [Rapport de recherche] 2011, pp.16. <inria-00568947>

Partager

Métriques

Consultations de
la notice

268

Téléchargements du document

165