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] proving false and counter examples

> It is difficult in this theoretical framework, which is optimized for
> the verification of powerful functional properties at the detriment of
> nice-to-haves such as the production of counter-examples.

I think counter examples are more than just nice to have.  Getting
tools like this widely adopted by industry will probably depend on
them.  In the ASIC industry, the only reason model checking has caught
to the extent it has is because when an RTL designer sees a counter
examples in a waveform viewer, they are in there comfort zone.  To
them it's just like debugging a simulation.

> As soon as
> there is a loop in the code, getting a false proof obligation ceases
> to mean that the specification is incorrect

But what about programs without loops?  And for loops, are there any
plans to use techniques from model checking?  I've have success with
k-induction in AFV [1] and I know the CBMC folks are using similar
methods [2] [3].

> PS: I don't want to seem to be promoting my own stuff too much, but
> the value analysis can tell that obviously false specifications are
> obviously false. It won't provide a counter-example expressed in terms
> of the function's inputs though, because it goes forward only.

Thanks.  I plan to check this out next week.

-Tom

[1] http://hackage.haskell.org/package/afv
[2] http://www.cprover.org/cbmc/
[3] http://www.kroening.com/papers/tacas2010-cellmc-draft.pdf