On system reliability and verification

In response to a paper by J.H. Fetzer (Commun. ACM, vol.31, p.1048-63, 1988) and the subsequent decision, a clarification is given of what is meant by program verification and what are its benefits and limitations. An explanation is presented as to why formal verification can only, at best, guarantee the correct operation of an algorithm. For real systems (e.g. a program running on a real machine) all one can aim for is to achieve a high degree of confidence that the design is correct. This is done by applying validation techniques (e.g. testing, debugging, simulation, formal verification, etc.), fault-tolerant techniques, and good design methods. A comparison is made of the methods of science with the methods used in software design with regard to verification