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
Document type :
Reports
Complete list of metadatas

https://hal.inria.fr/inria-00568947
Contributor : Nicolas Stouls <>
Submitted on : Thursday, February 24, 2011 - 7:55:19 AM
Last modification on : Wednesday, November 28, 2018 - 9:36:02 AM
Long-term archiving on : Wednesday, May 25, 2011 - 2:37:36 AM

Files

main.pdf
Files produced by the author(s)

Identifiers

  • 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⟩

Share

Metrics

Record views

357

Files downloads

190