A. Cafe and . Frama, C se dote d'un outil de model-cheking qui traite efficacement des spécifications dans une logique temporelle expressive. Il permet également d'apprécier les interactions possibles entre différents outils qui, décorrélés, ne permettent pas de vérifier la spécification souhaitée. La suite du développement de CaFE est principalement axée sur l'explosion combinatoire, toujours problématique lors du traitement d'exemples industriels, et sur une recherche de contre-exemple plus efficace

]. R. Références1, M. Alur, K. Benedikt, P. Etessami, T. Godefroid et al., Analysis of recursive state machines, ACM TOPLAS, vol.27, issue.4, 2005.

R. Alur and K. Etessami, MADHUSUDAN : A temporal logic of nested calls and returns, TACAS 2004, pp.467-481, 2004.
DOI : 10.1007/978-3-540-24730-2_35
URL : https://link.springer.com/content/pdf/10.1007%2F978-3-540-24730-2_35.pdf

P. Baudin, J. Filliâtre, C. Marché, B. Monate, Y. Moy et al., , 2016.

S. Blazy and D. Bühler, YAKOBOWSKI : Structuring abstract interpreters through state and value abstractions, VMCAI 2017, Proceedings, pp.112-130, 2017.
DOI : 10.1007/978-3-319-52234-0_7

, CARBONELL : Polynomial invariant generation, E

L. M. De, M. , and N. Bjørner, Z3 : an efficient SMT solver, TACAS, Proceedings, pp.337-340, 2008.

S. De, O. , S. Bensalem, and V. Prevosto, Polynomial invariants by linear algebra, ATVA 2016, Proceedings, pp.479-494, 2016.

S. De, O. , V. Prevosto, and S. Bardin, Au temps en emporte le C, Actes des JFLA, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01099128

F. Kirchner, N. Kosmatov, V. Prevosto, J. Signoles, and B. Yako-bowski, Frama-C: A software analysis perspective, Formal Aspects of Computing, vol.12, issue.1???2, p.2015
DOI : 10.1007/11408901_21
URL : https://hal.archives-ouvertes.fr/cea-01808981

A. Pnueli, The temporal logic of programs, 18th Annual Symposium on Foundations of Computer Science (sfcs 1977), p.31
DOI : 10.1109/SFCS.1977.32