I've recently written an article (in two parts) over at Electronic Design about applying different methods of verification to the same small piece of code. The code in question is an implementation of binary search, and I applied Testing, Static Analysis (using the AdaCore tool CodePeer) and Formal Verification (using the AdaCore tool SPARK 2014).

In the First Part, I started with one implementation of binary search, applied a quite naive testing strategy, which appeared to be relatively comprehensive, and managed to find one bug. I then applied the CodePeer tool, which found another problem. In the Second Part, I wrote Ada 2012 contracts and applied the SPARK 2014 tool to the code. I not only found two more problems, but also managed to prove that the code is entirely free of run-time errors and always provides the correct answer.