CaFE

_fc-plugins/cafe.html

+---
+layout: plugin
+title: CaFE
+description: Verification of CaRet temporal logic properties
+key: specifications
+distrib_mode: free
+---
+
+<dl class="defnitionList">
+  <dt class="subTitle">Overview</dt>
+  <dd><p>CaFE (CaRet Frama-C Extension) is a small model-checker dedicated
+      to prove CaRet properties over C programs.
+      <a href="https://doi.org/10.1007/978-3-540-24730-2_35">CaRet</a> 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.
+    </p>
+  </dd>
+  <dt class="subTitle">Use</dt>
+  <dd>
+    <p><a href="https://github.com/Stevendeo/CaFE">CaFE</a> is available as a
+      separate open-source plug-in. Once installed, it will be activated by
+      the <tt>-cafe</tt> option, while <tt>-cafe-formula</tt> allows specifying
+      the file in which to formula to be verified lies. A typical command will
+      thus be the following:
+      <pre>frama-c -cafe file.c -cafe-formula file.caret</pre>
+    </p>
+    <p>Note that CaFE uses <a href="eva.html">Eva</a> internally to compute
+      an over-approximation of the states of the program.
+    </p>
+  </dd>
+</dl>