Can control theory make software better?

Techniques used to ensure that airplanes won't stall out in flight could be adapted to prove that computer programs won't divide by zero. "Formal verification" is a set of methods for mathematically proving that a computer program does what it's supposed to do. It's universal in hardware design and in the development of critical control software that can't tolerate bugs; it's common in academic research; and it's beginning to make inroads in commercial software. In the latest issue of the journal IEEE Transactions on Automatic Control , researchers from MIT's Laboratory for Information and Decision Systems (LIDS) and a colleague at Georgia Tech show how to apply principles from control theory - which analyzes dynamical systems ranging from robots to power grids - to formal verification. The result could help computer scientists expand their repertoire of formal-verification techniques, and it could be particularly useful in the area of approximate computation , in which designers of computer systems trade a little bit of computational accuracy for large gains in speed or power efficiency. In particular, the researchers adapted something called a Lyapunov function, which is a mainstay of control theory. The graph of a standard Lyapunov function slopes everywhere toward its minimum value: It can be thought of as looking kind of like a bowl.