Formal Algorithm Verification
Methods for getting your program’s ducks in a row.
Algorithms are programs whose only purpose is to perform a computation or run operations to solve a problem. It receives input, takes action upon the arguments, and provides an output.
So then, when we look at formal algorithm verification, what do we mean?
Software Testing vs. Formal Verification
Software testing is often done through peer reviews, code inspections, various levels of testing, demonstrations, and analysis. We poke, prod, and twist the code to try and shake out any problems.
However, it’s important to note that this form of testing only determines when an algorithm is not correct. Informal verification like this cannot prove 100% correctness because we can’t cover all test cases. That could include an infinite set of inputs!
With the popularity of agile methodologies and CI/CD pipelines, many applications can be rapidly fixed and re-deployed, contributing to the desire to stick with these types of industrial test methods. Corrections are usually straightforward to distribute quickly to users.
On the other hand, formal verification uses mathematical methods (such as “proof by induction”) to confirm the total…
