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]
[Frama-c-discuss] question about a simple example and jessie
- Subject: [Frama-c-discuss] question about a simple example and jessie
- From: pascal.cuoq at gmail.com (Pascal Cuoq)
- Date: Fri, 14 May 2010 01:06:53 +0200
- In-reply-to: <4BEC6D3B.8060105@cslabs.com>
- References: <4BDF2C15.5010201@cslabs.com> <x2xb15d09071005031421v51333b13ma27dc52ec76a51dc@mail.gmail.com> <4BEC6D3B.8060105@cslabs.com>
> I tried to do a sanity check by negating the post-condition and I still > get the green bullet for the post-condition. ?That doesn't sound right No it doesn't. Here are the possibilities: - there is or was a bug in the Frama-C toolchain, including Why but not the automatic provers. - one of the invariants is false, and your CVC3 is correctly using it to prove both the post-condition and its negation. This possibility further sub-divides into: * the students are lying weasels, * or the theorem prover that they used to check the invariants at the time was a lying weasel - there is a bug in the theorem prover that you are using now. Could you clarify what the diagnostic of each of alt-ergo and CVC3 is for your post-condition and its negation? This article mentions obtaining wrong diagnostics from some versions of CVC3, and switching to a "two different automated provers" criterion: http://arxiv4.library.cornell.edu/pdf/1004.5034v1 In the Challenger report I linked to in another thread, Richard Feynman has something to say about multiplying probabilities that have not been quantified to improve safety, I am sure. Meanwhile, research on certified/certifying automated provers is all the rage these days, but perhaps we users of existing provers could take advantage of the common front-end Why provides for these provers to build up a shared database of known true and false properties, and check the provers for correctness regressions? Pascal
- Follow-Ups:
- [Frama-c-discuss] question about a simple example and jessie
- From: naghmeh.ghafari at cslabs.com (Naghmeh Ghafari)
- [Frama-c-discuss] question about a simple example and jessie
- References:
- [Frama-c-discuss] question about a simple example and jessie
- From: naghmeh.ghafari at cslabs.com (Naghmeh Ghafari)
- [Frama-c-discuss] question about a simple example and jessie
- From: pascal.cuoq at gmail.com (Pascal Cuoq)
- [Frama-c-discuss] question about a simple example and jessie
- From: naghmeh.ghafari at cslabs.com (Naghmeh Ghafari)
- [Frama-c-discuss] question about a simple example and jessie
- Prev by Date: [Frama-c-discuss] question about a simple example and jessie
- Next by Date: [Frama-c-discuss] question about a simple example and jessie
- Previous by thread: [Frama-c-discuss] question about a simple example and jessie
- Next by thread: [Frama-c-discuss] question about a simple example and jessie
- Index(es):