[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