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

Jean-Christophe Filliatre Jean-Christophe.Filliatre at lri.fr
Wed Feb 29 16:08:51 CET 2012


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?

-- 
Jean-Christophe



More information about the Why3-club mailing list