Program verification is the process of formally proving that a computer program does exactly what is stated in the program specification it was written to realize.
See also Formal verification
