[Why3-club] [Why-discuss] Why3 PVS backend and Jessie
filali at irit.fr
Wed Feb 29 16:11:58 CET 2012
One could consider TLC: the model checker of TLA
Le 29mercredi/02/12 29 à 16: 51, Jean-Christophe Filliatre a écrit :
> 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?
> - do you have any model checker in mind whose logic is powerful enough
> to match the logic of Why3?
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 277 bytes
Desc: not available
More information about the Why3-club