[Why3-club] [Why-discuss] Why3 PVS backend and Jessie
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?
- 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
- do you have any model checker in mind whose logic is powerful enough
to match the logic of Why3?
More information about the Why3-club