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

[Frama-c-discuss] Inductive definition of reachability in an array-implemented list.



Dear Eric and Jens,

I will try to give a global response, but "jessie Masters" are still Yannick Moy 
and Claude March? O:-)

The conversion Integer -> int is not costless for automatic provers. The "exact" 
option removes conversion predicates. It is then more efficient. However, is 
there any sense to prove a program without these conversions ?

In my opinion, there is really 2 disjoint goals :
    * is my program correct without machine constraints ? (abstract Integers)
        --> exact option

    * are abstract values equals to concrete ones in previous PO ?
        --> if yes : just smile
            if not : same player play again, but without exact option.

I don't know how to verify this second point. But I think that if a PO is valid 
with Integers and timeout without, then a manual proof can be tried.

Regards,
Nicolas.




JENN Eric a ?crit :
> As a followup to Jens' previous message (and to Nicolas answer to my 
> previous question), here is the translation of a message I sent directly 
> to Nicolas, in order to avoid cluttering the mailing list with my 
> (newbye) questions. Well, I think that it may be useful (not the 
> questions, but the answers to come...).
> 
> "Actually, if I think that if I basically understand the differences 
> between those options (not their actual effect, but their meaning), I 
> miss some information to make an "operational choice": as I can't use 
> the strictiest model all the time, how shall I proceed?
> 
>  From what you write, I guess an approach could be to (i) try to verify 
> all properties using the most constraining integer model, (ii) finalize 
> the proof of properties that can't be verified with these constraints by 
> relaxing the integer model and (iii) demonstrate (one way or another) 
> that no overflow may occur for those variables considered "exact" rather 
> than "bounded or modulo".
> 
> This specific problem is part of a bigger set of issues: /how shall I 
> write my pre, post, invariants to optimize the probability for all POs 
> to be automatically discharged? How shall I handle a PO that lead to a 
> timeout? (How do I analyze the problem?), Why are some POs discharged 
> with one prover while another prover shows the"danger sign" ? What does 
> it mean? etc. "/
> 
> I guess that I'll find an answer to all those questions while time 
> passes and my close-to-null experience grows!  Unfortunately, time is a 
> bit missing over there...
> 
> Regards,
> 
> Eric.
> 
> _______________________________________________
> 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/20090605/7f470c6f/attachment.vcf