--- layout: fc_discuss_archives title: Message 46 from Frama-C-discuss on May 2010 ---
> 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