[Why3-club] [Why-discuss] Why3 PVS backend and Jessie

Nuno Gaspar nmpgaspar at gmail.com
Wed Feb 29 14:52:36 CET 2012

Following this out of topic discussion, just wondering:

 Is there any particular reason why there haven't been so far any works
connecting Why3 (or Why2 for that matter...) to a Model Checker?
Would you consider irrelevant/senseless to have such a driver?

I mean, would you say that VCs produced by Why3 and not discharged by an
SMT would very unlikely be handled by a Model Checker?

2012/2/29 Jean-Christophe Filliatre <Jean-Christophe.Filliatre at lri.fr>

> On 29/02/2012 10:58, Nuno Gaspar wrote:
>> slightly out of topic: Are there any plans for Isabelle support?
> As we used to do with Why 2.xx, the addition of a new driver is done "on
> demand". Since two different persons asked for some Isabelle driver today,
> we may now consider building one.
> Of course, contributions are welcome. If one contributes it, we'll gladly
> integrate it in Why3 distribution. Especially if it comes from someone who
> is more familiar with Isabelle than I am.
> --
> Jean-Christophe
> ______________________________**_________________
> Why3-club mailing list
> Why3-club at lists.gforge.inria.**fr <Why3-club at lists.gforge.inria.fr>
> http://lists.gforge.inria.fr/**cgi-bin/mailman/listinfo/why3-**club<http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/why3-club>

Bart: Look at me, I'm a grad student, I'm 30 years old and I made $600
dollars last year.
Marge: Bart! Don't make fun of grad students, they just made a terrible
life choice.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/why3-club/attachments/20120229/650b3198/attachment.htm>

More information about the Why3-club mailing list