cafe.md

---
layout: plugin
title: CaFE
description: Verification of CaRet temporal logic properties
key: specifications
distrib_mode: free
repo_url: https://github.com/Stevendeo/CaFE
---

## Overview

CaFE (CaRet Frama-C Extension) is a small model-checker dedicated
to prove CaRet properties over C programs.
[CaRet](https://doi.org/10.1007/978-3-540-24730-2_35) is
"a temporal logic of nested calls and returns", i.e. a flavor of
temporal logic well suited to describe a program's call stack.

## Usage

[CaFE]({{page.repo_url}}) is available as a
separate open-source plug-in. Once installed, it will be activated by
the `-cafe` option, while `-cafe-formula` allows specifying
the file in which to formula to be verified lies. A typical command will
thus be the following:

    frama-c -cafe file.c -cafe-formula file.caret

## Dependencies

CaFE uses [Eva](eva.html) internally to compute an over-approximation
of the states of the program.