[gvr]

That is certainly one source for error. There are many. Another is that testing does not give you exhaustive coverage of the state space just because each branch of the code is visited.

The standard does mention "formal verification/methods/proof" but to my knowledge it's rarely been used extensively.

[wyldfire]

Mathworks makes a sat solver kinda product that does those kinds of proofs. Pretty interesting concept, IMO.