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