What is CaFE ?
CaFE (for Caret Frama-c's Extension) is a model-checker being developped in the Frama-C framework. It is based on the temporal logic CaRet, a temporal logic based on Call and Return properties.
CaFE uses the results of Value , a powerful static analyser in Frama-C, in order to generate a recursive state machine over which it performs a model-checking procedure. It is not open source, but it is described in this french article.
Presentation of CaFE with Pilat at the Frama-C days 2016 : poster.