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

> 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