Skip to Main content Skip to Navigation
Conference papers

CaFE : un model-checker collaboratif

Steven de Oliveira 1 Virgile Prévosto 1 Saddek Bensalem 2
1 LSL - Laboratoire Sûreté des Logiciels
DILS - Département Ingénierie Logiciels et Systèmes : DRT/LIST/DILS
Résumé : 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.
Document type :
Conference papers
Complete list of metadata

Cited literature [11 references]  Display  Hide  Download

https://hal-cea.archives-ouvertes.fr/cea-01835522
Contributor : Virgile Prevosto Connect in order to contact the contributor
Submitted on : Wednesday, July 11, 2018 - 2:26:09 PM
Last modification on : Wednesday, November 3, 2021 - 4:29:46 AM
Long-term archiving on: : Saturday, October 13, 2018 - 1:59:11 AM

File

main.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : cea-01835522, version 1

Citation

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⟩

Share

Metrics

Record views

503

Files downloads

119