--- layout: fc_discuss_archives title: Message 9 from Frama-C-discuss on December 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Which version of Frama-C/Why to use PVS ? (Jessie or WP)



Hi all,

Could anybody clarify the current state of the various tools: Frama-C Oxygen/Nitrogen/WP/Jessie/PVS5/PVS6? I would like to use the PVS backend of Why for deductive methods.

It should work with:
- Nitrogen + Jessie + Why 2 + PVS 5
- Nitrogen + Jessie + Why 2 (to have Jessie) + Why 3 + PVS 6 (not yet released)
- Oxygen + ???

Jessie is not yet usable with Oxygen. On the other hand, Oxygen/WP does not seem to allow to use the PVS backend of Why:
-wp-proof <dp,...>  Submit proof obligations to external prover(s):
                    - 'none' to skip proofs
                    Directly supported provers:
                    - 'alt-ergo' (default)
                    - 'altgr-ergo' (gui)
                    - 'coq', 'coqide' (see also -wp-script)
                    Supported provers via Why:
                    - 'simplify', 'vampire', 'yices', 'cvc3', 'z3', 'zenon'

My question is the following: is it possible to generate a Why2 or Why3 proof obligation with Oxygen/WP and use Why2 PVS backend ?

Kind regards,

pl
-- 
Pierre-Lo?c Garoche
Research Scientist @ ONERA
pierre-loic.garoche at onera.fr - pierre-loic-garoche at uiowa.edu
http://www.onera.fr/staff/pierre-loic-garoche/
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 198 bytes
Desc: Digital signature
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20121218/a155bcf7/attachment.pgp>