Correctness of algorithms



An algorithm is correct if it produces the expected output for each input.

Partial and total correctness

An algorithm is only partially correct if may not terminate. Otherwise it is totally correct.

Formal verification

Model checking

Model checking allows the formal verification of algorithms with finite inputs. test every possible input.

Deductive verification

Check the parts of the algorithm using theorem provers.