Frama-C-discuss mailing list archives
This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
- Subject: No subject
- From: firstname.lastname@example.org ()
- Date: Wed, 03 Jun 2009 13:41:51 -0000
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". <br> <br> This specific problem is part of a bigger set of issues: <i>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><br> <br> 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... <br> <br> Regards,<br> <br> Eric.<br> </body> </html> --------------040503090609060209050008 Content-Type: text/x-vcard; charset=utf-8; name="eric.jenn.vcf" Content-Transfer-Encoding: 7bit Content-Disposition: attachment; filename="eric.jenn.vcf" begin:vcard fn:Eric JENN n:JENN;Eric org:Thales Avionics;AMS / MMAC adr;quoted-printable;dom:;;105, avenue du G=C3=A9n=C3=A9ral Eisenhower;Toulouse x-mozilla-html:TRUE version:2.1 end:vcard --------------040503090609060209050008--