--- layout: fc_discuss_archives title: Message 46 from Frama-C-discuss on May 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] question about a simple example and jessie



> 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