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