Program verification

In computer science, 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. It is an instance of Formal verification (and more generally Formal methods). Program verification is more specific in that it aims to verify the code itself, not only some abstract model of the program.

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.