ABSTRACT

When a program is implemented to provide a concrete representation of an algorithm, the developers of this program are naturally concerned with the correctness and performance of the implementation. Software engineers must ensure that their software systems achieve an appropriate level of quality. Software verification is the process of ensuring that a program meets its intended specification [Kaner et al., 1993]. One technique that can assist during the specification, design, and implementation of a software system is software verification through correctness proof. Software testing, or the process of assessing the functionality and correctness of a program through execution or analysis, is another alternative for verifying a software system. As noted by Bowen and Hinchley [1995] and Geller [1978], software testing can be appropriately used in conjunction with correctness proofs and other types of formal approaches to develop high-quality software systems. Yet it is also possible to use software testing techniques in isolation from program correctness proofs or other formal methods.