In recent years the subject of program verification has sat firmly within the realm of academic theoretical computer science, and has had very little impact on the computing industry. This is despite its potential for long term cost savings, and the avoidance of embarassing project failures.
Software testing on the other hand, forms a major and respected activity in most industrial software engineering projects, despite the fact that its scientific basis is largely undeveloped and its motivation often poorly understood by the academic community.
After a brief review of these two subjects, we will show how they form two sides of the same scientific coin. Academic formal methods by tradition focuses on proof construction to demonstrate correctness. Test engineers, usually manually, carry out activities closely related to model generation to demonstrate the presence of errors. Though this scientific description of their work is almost never made explicit in their literature. The familiar Gödel Completeness Theorem is the bridge between these two activities.
The duality between these two approaches becomes significant when we begin to consider the kinds of algorithms required by each community. In particular, an efficient algorithm for one activity can often be applied to the other with beneficial results.
Back to Karl Meinke's Home Page