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

Mamoun FILALI-AMINE 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...
Name: filali.vcf
Type: text/x-vcard
Size: 277 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/why3-club/attachments/20120229/a05fc0de/attachment.vcf>

More information about the Why3-club mailing list