Steven de Oliveira

Ph.D. Student in formal methods

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.