Traditional verification methods

1. Inductive invariants have been used in proving the correctness of sequental algorithms. Nowadays they are used in hardware verification, too.
2. Process algebras and equivalences. The idea is to specify a system as well as the service it produces as a process-algebraic expression and then prove that these are equivalent. There are a couple of problems with this approach. First, process-algebraic expressions tend to be too large even for a computer in many practical situations. Secondly, it is not easy always to specify the service a protocol or system produces. But if a system is of right size and its service can be specified, this approach is very elegant.
3. Temporal logics. Again a system is specified using a process algebra or some other specification formalism. Then, using temporal logic, it is shown that the systems satisfies the required properties. This approach is easier than the equivalence-based verification, if a service cannot be described clearly. Otherwise, this approach suffers of state explosion, too.
4. Several methods have been developed to avoid the state explosion problem. These include, for example, binary decision diagrams, partial order methods and interface specifications.