Testing is a cornerstone of quality software design. And yet, it’s time consuming, labor and resource intensive, and extremely difficult to do exhaustively. In fact, most software in use today is so complex that thorough testing is practically impossible.
A group of researchers from U-M envision a smarter alternative: why not let math do the heavy lifting of testing? Enter formal verification, a means to demonstrate that a program or algorithm is correct and reliable with all the elegance of a logical proof.
Unfortunately, while testing is certainly time consuming, writing proofs about a piece of code or an algorithm is usually even worse on that front — so far, anyway. That’s why a primary early motivation for the team from the College of Engineering was automating the process.
That means more than speeding up a testing alternative, it means a whole new paradigm in security and reliability. A formal automated verification process will enable entire libraries of complex, reusable code that is certified safe and ready to deploy, saving developers time, money, and anxiety.
