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
- Subject: [Frama-c-discuss] proving false and counter examples
- From: pascal.cuoq at gmail.com (Pascal Cuoq)
- Date: Sun, 9 May 2010 02:14:35 +0200
- In-reply-to: <w2n594c1e831005081638of517d0e6n2ebf1548880c3210@mail.gmail.com>
- References: <u2y594c1e831005081010z45bf5d50k99abc673fc14a451@mail.gmail.com> <o2yb15d09071005081036vecac7ef2p310a53ce13c2afa1@mail.gmail.com> <w2n594c1e831005081638of517d0e6n2ebf1548880c3210@mail.gmail.com>
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
- References:
- [Frama-c-discuss] proving false and counter examples
- From: tomahawkins at gmail.com (Tom Hawkins)
- [Frama-c-discuss] proving false and counter examples
- From: pascal.cuoq at gmail.com (Pascal Cuoq)
- [Frama-c-discuss] proving false and counter examples
- From: tomahawkins at gmail.com (Tom Hawkins)
- [Frama-c-discuss] proving false and counter examples
- Prev by Date: [Frama-c-discuss] proving false and counter examples
- Next by Date: [Frama-c-discuss] frama-c boron inconsistency with beryllium
- Previous by thread: [Frama-c-discuss] proving false and counter examples
- Next by thread: [Frama-c-discuss] frama-c boron inconsistency with beryllium
- Index(es):