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

Nuno Gaspar nmpgaspar at gmail.com
Wed Feb 29 16:52:41 CET 2012

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

> On 29/02/2012 14:52, Nuno Gaspar wrote:
>> 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?
> To clarify:
> - by "handled by a Model Checker", do you mean "proved valid by a model
> checker" or do you mean that a counterexample could be generated by a model
> checker?

I meant proved valid. With the possibility of validating or not some model
generated by Why3, I guess that generation of counter examples would follow
"for free", since it would be a purely model checking concern then..

> - do you have any model checker in mind whose logic is powerful enough to
> match the logic of Why3?

Well, since it would be Why3 to feed the model checker, I think the
question is more of whether is it possible (and relevant) to define a
driver that would allow the encoding of Why3 models that could be handled
by a MC.

Consider this:

Defining a Why3 theory for dealing for a very specific domain. Producing
models that fits this theory would allow to benefit from having several
deductive provers at hand.

Now assuming a scenario where all but one subgoal are discharged. We could
imagine that Why3 tried to use a MC to discharge the last one. Since we
would be dealing with this very specific domain having a powerful enough
logic would not be a problem I guess, since the problem itself started from
a very specific domain (that say, is usually dealt by Model Checkers..) .
And thus allowing to 'combine' deductive methods with MC...

I'm probably not being very clear :), anyway, I was just wondering about
this apparent "lack". There are some works integrating MC with ITP, namely
with Isabelle, so I was just wondering about Why3.

Not sure about TLA+, may worth checking. thanks!

> --
> Jean-Christophe

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/c7fc90ba/attachment.htm>

More information about the Why3-club mailing list