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