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

On Sun, May 9, 2010 at 1:38 AM, Tom Hawkins <tomahawkins at gmail.com> wrote:
>> 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.

The verification of critical software operates under completely different rules.
It is the kind of world about which Richard Feynman wrote, when he was
trying to find something that was worked in the Challenger shuttle:
"Such unexpected errors have been found only about six times in all
the programming and program changing (for new or altered payloads)
that has been done. The principle that is followed is that all the verification
is not an aspect of program safety, it is merely a test of that safety, in a
non-catastrophic verification."

The software already works when it is being verified. Anything that seems
wrong during verification, any "alarm", is a false alarm.
You don't spend time designing a tool that looks for a counter-example in
these conditions, because there is no counter-example, only a (theoretically
more or less unavoidable) weakness in the tool.

> And for loops, are there any
> plans to use techniques from model checking?

Any technique that works for software verification can be implemented
as a Frama-C plug-in and we'll be glad to see it happen. Existing
plug-ins are biased towards the verification of critical code, but the
framework has no restriction in this respect (from the other end
of the spectrum, there will be a presentation
of coding rules verification plug-ins at ERTS this month).
If you have ideas, please do not hesitate to put them in practice.
But to be frank, if we were following suggestions from this mailing-list,
we'd be busy writing our own C preprocessor so that users
do not need to provide theirs. That's what the last suggestion was.

There are industrial partners who have been experimenting with the tools
that we make available, and who have shown what they could do with
what was already available. We trust them to be taking us in the right
direction when they ask for evolutions, because it's in
everyone involved's interest.

Pascal