--- layout: fc_discuss_archives title: Message 42 from Frama-C-discuss on April 2011 ---
Hello, On Mon, Apr 25, 2011 at 6:15 PM, Eugene Kornykhin <kornevgen at gmail.com> wrote: > Is it possible to translate PVS to any representation for Frama-c ? Is > there any tool to translate PVS to Frama-C ? I have tool which > generates PVS theory from specification, and I'm interesting whether > is it possible to use Frama-c (with many provers as backends) to prove > PVS theory. You may be confusing Frama-C with Why: http://why.lri.fr/ Why is indeed used as a component inside Frama-C, but not all Frama-C plug-ins use Why, and it is not Why's sole purpose to be used in Frama-C. You should probably ask on Why's mailing list: http://lists.gforge.inria.fr/mailman/listinfo/why-discuss Pascal