Program Verification - the process of formal proving, that the Computer program does exactly what is stated in the program specification it was written to realize.

See Also Turing machine