CaFE : un model-checker collaboratif - CEA - Commissariat à l’énergie atomique et aux énergies alternatives Access content directly
Conference Papers Year :

CaFE : un model-checker collaboratif

Virgile Prévosto
Saddek Bensalem

Abstract

La logique temporelle linéaire (LTL) est utilisée dans de nombreux travaux pour décrire formellement le comportement attendu d'un programme. Une extension particulièrement intéressante de LTL pour l'analyse de programmes est la logique $CaRet$, qui autorise des raisonnements explicites sur la pile d'appel. Ce papier présente $CaFE$ , un greffon de la plate-forme $Frama$-C qui vérifie automatiquement de manière approchée qu'un programme C vérifie une formule logique $CaRet$ donnée. Il décrit également la mise en oeuvre de $CaFE$ et ses interactions avec le reste de la plate-forme.
Fichier principal
Vignette du fichier
main.pdf (592.63 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

cea-01835522 , version 1 (11-07-2018)

Identifiers

  • HAL Id : cea-01835522 , version 1

Cite

Steven de Oliveira, Virgile Prévosto, Saddek Bensalem. CaFE : un model-checker collaboratif. Approches Formelles pour l'Assistance au Développement du logiciel - AFADL, Jun 2017, Montpellier, France. ⟨cea-01835522⟩
68 View
81 Download

Share

Gmail Facebook Twitter LinkedIn More