### Article Author

### Date Published

March 19, 2013

### Link to Original Article

“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. If the function characterizes the dynamics of a physical system, and the minimum value represents a stable state of the system, then the curve of the graph guarantees that the system will move toward greater stability.

Of course, most dynamical systems are more complex than pendulums, and finding Lyapunov functions that characterize them can be difficult. But there’s a large literature on Lyapunov functions in control theory, and Roozbehani and his colleagues are hopeful that much of it will prove applicable to software verification.

#### Skirting dangers

In their new paper, Roozbehani and his coauthors — MIT professor of electrical engineering Alexandre Megretski and Eric Feron, a professor of aerospace software engineering at Georgia Tech — envision a computer program as a set of rules for navigating a space defined by the variables in the program and the memory locations of the program instructions. Any state of the program — any values for the variables during execution of a particular instruction — constitutes a point in that space. Problems with a program’s execution, such as dividing by zero or overloading the memory, can be thought of as regions in the space.

In practice, finding a Lyapunov invariant with the desired properties means systematically investigating different classes of functions. There’s no general way to predict in advance what type of function it will be — or even that it exists. But Roozbehani imagines that, if his and his colleagues’ approach catches on, researchers will begin to identify algorithms that lend themselves to particular types of Lyapunov invariants, as has happened with control problems and Lyapunov functions.

#### Fuzzy thinking

Moreover, many of the critical software systems that require formal verification implement control systems designed using Lyapunov functions. “So there are intuitive reasons to believe that, at least for control-system software, these methods will work well,” Roozbehani says.

Roozbehani is also enthusiastic about possible applications in approximate computation. As he explains, many control systems are based on mathematical models that can’t capture all of the complexity of real dynamical systems. So control theorists have developed analytic methods that can account for model inaccuracies and provide guarantees of stability even in the presence of uncertainty. Those techniques, Roozbehani argues, could be perfectly suited for verifying code that exploits approximate computation.

“The idea may not apply in all possible kinds of software,” Pappas cautions. “But if you’re thinking about software that implements, say, controller or sensor functionality, I think there’s no question that these types of ideas will have a lot of impact."

Reprinted with permission of MIT News.