The Jessie plug-in allows deductive verification of C programs annotated with ACSL. It uses internally the languages and tools of the Why platform. The generated verification conditions can be submitted to external automatic provers such as Simplify, Alt-Ergo, Z3, Yices, CVC3.
For more complex situations, interactive theorem provers can be used to establish validity of VCs. Please look at the Jessie web page for more details.
The plug-in is activated with the following command line:
frama-c -jessie [options] <file>.c
A short manual including a tutorial and reference is available on the Jessie Web page. Please read this document for details on other command-line options and supported or unsupported features.