--- layout: fc_discuss_archives title: Message 10 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)



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