--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on December 2012 ---
On 12/18/2012 01:09 PM, Pierre-Lo?c Garoche wrote: > 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 Interesting question, I would like to have an answer as well. We use old chain: - Nitrogen + Jessie + Why 2 + PVS 5 and we would like to know possible update paths. -- Best, Alexey Khoroshilov Linux Verification Center, ISPRAS web: http://linuxtesting.org