News Release

Verifying the Logic of
Computer Programs

For further information, contact:
Dr. Robert P. Kurshan
Bell Laboratories, Murray Hill, NJ
Telephone: 908-582-4511
Email: k@research.bell-labs.com

April 12, 2000

PROVIDENCE, RI---The cause of the catastrophic crash of the Ariane 5 rocket in 1996 was traced to a simple problem in the computer software that calculated the rocket's position. Despite rigorous testing of the software, the problem went unnoticed. Such software failures occur every day---though usually with less spectacular consequences.

How can one insure that computer programs actually do what they are intended to do? Simply running a program repeatedly with various inputs is inadequate, because one cannot tell which inputs might cause the program to fail. It is possible to tailor a tester to test a given program, but present-day programs are so complex that thay cannot be adequately checked through conventional testing, which can leave significant bugs undetected.

A different way to approach this problem is to try to find methods of examining the internal logic of computer programs. In the enclosed article, Robert P. Kurshan describes such a method called "program verification", which, instead of executing a program to check it, uses mathematics to analyze its logic.

Program verification can increase the reliability of a computer program by checking it in ways that may be overlooked in conventional testing. One of the virtues of program verification is that it can be used to verify the correctness of segments of a program as they are created. By contrast, most conventional testing methods can only be carried out at the end of the program development cycle.

Commercial products incorporating program verification are today mostly used in integrated circuit manufacturing. "However, the program verification methodologies described here can be applied to significant portions of general software development," Kurshan writes, "and this is the direction of the industry."

The article "Program Verification" appears in the May 2000 issue of Notices of the AMS. A PDF file containing the article may be downloaded at http://www.ams.org/notices/200005/fea-kurshan.pdf.