--- layout: fc_discuss_archives title: Message 43 from Frama-C-discuss on April 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] How to translate PVS to Frama-c



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
>