--- layout: fc_discuss_archives title: Message 43 from Frama-C-discuss on April 2011 ---
Thank you, Pascal. Eugene 2011/4/25 Pascal Cuoq <pascal.cuoq at gmail.com>: > 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 > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss >