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.