New method ensures complex programs are bug-free without testing

(Five spools of yarn — two pink, one purple, two blue — each with a string of yarn extended out, tied to the others.) — Multithreading is one common form of concurrent execution, allowing different instructions in a program to be processed simultaneously by one or more CPU cores. (Courtesy U-M’s College of Computer Science and Engineering.)

A team of researchers from the University of Michigan, Microsoft Research, and Carnegie Mellon have created Armada, a system that uses a technique called formal verification to prove whether a piece of software will output what it is designed to produce without bugs.

Armada targets software that uses concurrent execution, a method of performance boosting, and passes systems through a series of transformations until they break down into simpler representations. The developer only has to prove that each simplified step accurately represents the more complex program from the previous step by using Armada’s high-level syntax to describe the simpler program and indicate a proof method that’s needed to support the transformation.

The automatically-generated proof runs through a prover for verification. If it fails, the user changes their description or proof method to make a new one.