[Why3-club] [Why-discuss] Why3 PVS backend and Jessie
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.
> Why3-club mailing list
> Why3-club at lists.gforge.inria.**fr <Why3-club at lists.gforge.inria.fr>
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
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Why3-club