Building a testing-free future

By | January 11, 2021
Jigsaw puzzle image of a padlock on a computer screen with hands putting in the pieces.
A group of U-M researchers uses mathematical proofs to demonstrate that software meets specifications for safe, correct execution without the need for traditional testing. (Karen Parker Moeller, MOEdesign)

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.