Program verification

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.

For functional programming languages, some programs can be verified by equational reasoning, usually together with induction. Code in an imperative language could be proved correct by use of Hoare logic.

This computer science article is a stub. You can help Wikipedia by expanding it.

See also