--- layout: fc_discuss_archives title: Message 35 from Frama-C-discuss on April 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Verification of axiomatization



Thank you very much to all.
An assert 0<>0 can't be automatically proved currently (With a timeout=400). 
Then I will probably try the second method : a coq model.

Best regards,
Nicolas.

Claude March? a ?crit :
> 
> Claude March? wrote:
>> I don't understand why you are so pessimistic, Pascal.
>> The answer is simple: just realize your axiomatization in Cuoq. Sorry: I 
>> meant in Coq.
> 
> Another, probably quicker, possibility is first to try to prove
> 
> //@ lemma l : 0=0;
> 
> from your axiomatization. If it is proven, then yes surely you have to 
> investigate you axiomatization. A way to do it then is to remove parts 
> of it until you discovered the eaxt subset of axioms that can derive false.
> 
> And if the lemme is not proven, then you might also try to prove
> 
> //@ assert 0=0;
> 
> just before return statement of the function that should not be proved 
> so quickly. And then proceed the same to remove some part of axiomatization.
> 
> Hope this helps,
> 
> - Claude
> 
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
-------------- section suivante --------------
Une pi?ce jointe non texte a ?t? nettoy?e...
Nom: nicolas_stouls.vcf
Type: text/x-vcard
Taille: 445 octets
Desc: non disponible
Url: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090407/a15d22f9/attachment.vcf