 |
Conference papers
CaFE : un model-checker collaboratif
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.
Cited literature [11 references]
https://hal-cea.archives-ouvertes.fr/cea-01835522
Contributor : Virgile Prevosto <>
Submitted on : Wednesday, July 11, 2018 - 2:26:09 PM
Last modification on : Friday, November 20, 2020 - 1:08:01 PM
Long-term archiving on: : Saturday, October 13, 2018 - 1:59:11 AM
Contributor : Virgile Prevosto <>
Submitted on : Wednesday, July 11, 2018 - 2:26:09 PM
Last modification on : Friday, November 20, 2020 - 1:08:01 PM
Long-term archiving on: : Saturday, October 13, 2018 - 1:59:11 AM
File
main.pdf
Files produced by the author(s)