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



> With Oxygen : there is no direct support for PVS at all, unless via Why-2

What would be the command or the options to use to produce a why2 proof obligation that could be later exported to pvs ?

The various options of Oxygen/WP do not mention why as a target prover.

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/20121219/5d6f6245/attachment.pgp>