--- layout: fc_discuss_archives title: Message 17 from Frama-C-discuss on April 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] which provers to use



Hi all, I have Frama-C working with the Jessie plugin (thanks for help everyone), but the only prover I have managed to get working is CVC3.  I have read some of the Why web pages but am a little confused about what is supported.  I've installed why2 and why3, and the latest Alt-Ergo, Z3, cvc3, and Gappa.

Here's my report from why2-config:

    prover      version              info   invocation
------------------------------------------------------
  Alt-Ergo       0.95.1   (not supported)   alt-ergo 
  Simplify                      not found   
   Vampire                      not found   
        Z3        4.3.2   (not supported)   z3 -smt 
     Yices                      not found   
      CVC3        2.4.1                     cvc3 -lang smt 
      CVCL        2.4.1                     cvc3 
     Gappa       0.17.1   (not supported)   gappa 
       Coq                      not found   
       PVS                      not found   
     VeriT                      not found   
     Zenon                      not found   
------------------------------------------------------

When I run frama-c -jessie, the why3ide shows only CVC3.  Should I be looking for older versions of some of these provers that are compatible with why?