--- layout: fc_discuss_archives title: Message 27 from Frama-C-discuss on July 2009 ---
Hi! This is an interesting question, and I am not surprised that you found different answers for it. I will provide one point of view. > I wonder about a general question. When is a proof considered to be > sufficient and exhaustive? It all depends on the objectives you have. It is not our (us tool providers) place to define them. To use an example, avionics software is usually written according to the guidelines defined in the DO-178B. The DO-178B is a rather general document, and the way it is actually implemented (by the aircraft manufacturer) is checked by the appropriate authority (the FAA, the EASA). In the DO-178B, tools that are used in the process have to be qualified (by the manufacturer): as development tools for things such as compilers, and as verification tools for tools used in verification. The qualification of a tool as development tool is an extremely heavy process. In comparison, the qualification as a verification tool is lighter, but still a significant piece of work. The aircraft manufacturer, not the tool provider, defines the usage that is made of the tool during the verification process, and shows the steps that were taken in order to check that the tool could be used reliably for this purpose. According to http://en.wikipedia.org/wiki/DO-178B , *comprehensive* (emphasis mine) black-box testing is currently judged sufficient for qualifying a tool as a verification tool. In short, if you need to trust any part of the Frama-C platform, you should first define your needs and make sure yourself that it suits them. Best regards, Pascal PS: I will be immodest enough to point to http://rdn-consulting.com/blog/2009/06/04/guest-article-static-analysis-in-medical-device-software-part-2-methodology/ and I also recommend the last section of http://tr.im/RPFeynman for an overview of how software verification works (although the Shuttle's software was verified using testing techniques only, to the best of my knowledge)