--- layout: fc_discuss_archives title: Message 9 from Frama-C-discuss on December 2012 ---
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>