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



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