Jessie

Overview

Warning Jessie is currently not actively maintained and probably incompatible with the latest Frama-C versions.

The Jessie plug-in allows deductive verification of C programs annotated with ACSL. It uses internally the languages and tools of the Why3 environment. The generated verification conditions can be submitted to many external automatic provers including Alt-Ergo, Z3 and CVC4.

For more complex situations, interactive theorem provers can be used to establish validity of VCs. While pages related to Jessie are now mostly inaccessible, a few examples are still available on this page

Usage

The plug-in is activated with the following command line:

frama-c -jessie [options] <file>.c