Methods for teaching program verification
Susan L. Gerhart · 1975
“Program verification” is generally defined as the process of ascertaining and demonstrating that a program is correct, i.e., that a program satisfies a given set of specifications. The most common method of verifying a program is by testing, the process of executing a program for a set of selected inputs and inferring from the results of those executions that the program is correct for all possible inputs.