Guest_Jim_* - March 20, 2013 02:35PM in Science & Technology

There are many fields and disciplines of science and each has its own distinct and valuable purpose, such as control theory which considers dynamical systems and formal verification, an important mathematical tool. Formal verification is used to rigorously prove a system is free of errors, so a formally verified computer program would never crash or do anything it should not. Most pieces of commercial software never undergo formal verification, but researchers at MIT have recently crafted a way to use control theory to ease its adoption by software companies.

A classic kind of function within control theory is the Lyapunov function which can be imagined as a pendulum. The vectors of a pendulum swinging always have it tending towards a stable minimum, so it is not possible for a pendulum to swing further on one swing than the previous. The researchers suggest applying this to software by considering every state of the program a point on a graph, with errors the program may run into treated as regions of the graph. By showing that no initial condition, no obtainable state of the software can be placed in the error-regions, it is possible to show the program cannot crash. The only catch is that this work can only be done on a case-by-case basis, and not in general.

Potentially this method of formally verifying software can also be used to enable approximate computation within software. Approximate computation allows a computer to use less-exact and less computational intensive methods, in order to speed up operation and reduce power requirements.

Source: MIT