The same year, Mars Polar Lander is suspected of having crashed on Mars upon landing when a software flag was not reset properly.

In contrast to those failures, the 1997 Mars Pathfinder (MPF) technology demonstration mission was considered a huge success when its Sojourner rover rolled about 100 yards across the planet in 87 days -- far exceeding its life expectancy of seven days. However, a day's exploration time was lost when ground support teams were forced to reboot the system while downloading science data.

Bugs are inevitable, but they must be uncovered early to ensure the most reliable software at the lowest cost. It is estimated that about half of software development costs are attributed to making sure the coding is correct. Considering the price of a space mission, the cost of an error could range from thousands of dollars during development to millions once a mission is under way.

NASA's 2003 Mars Exploration Rover (MER) mission includes two rovers scheduled to land on the Martian surface in January 2004 to sample rocks, soils and the atmosphere for at least 90 days.

At a cost of $400 million for each rover, a coding error that shuts down a rover overnight would in effect be a $4.4 million mistake, as well as a loss of valuable exploration time on the planet.

To catch such problems in the software code that flies during missions, NASA Ames is developing a software verification and validation technique to find flaws automatically, faster and more precisely than before.

"We detect what can interrupt the program, what can cause the program to crash," said researcher Guillaume Brat.

Software systems driving missions such as MER contain hundreds of thousands of lines of code that NASA developers currently test manually by writing test drivers and running tests as they write the code. The task is time-consuming and cumbersome. Furthermore, NASA's large systems with real-time decision capability are difficult to develop and validate because the possibilities for outcomes are so vast.

Brat is part of a team of two developing C Global Surveyor (CGS), a software based on the theory of abstract interpretation, a technique pioneered in the 1970s that hides all the data except what is necessary for finding errors. The technique detects errors automatically. It covers all possible execution paths without ever executing the program. Using a tool like CGS can save developers countless hours debugging code, said researcher Arnaud Venet. "You make the computer work for you instead of spending hours doing it."

With CGS, Brat said, "We can reason about all the behaviors with the program at once without having to go through each one of them."

Since its inception, just a few researchers have worked with abstract interpretation, trying to prove that the technique is practical. At present, just 20 or so people in the world might be working to develop efficient algorithms for the technique.

The CGS team started its research with tests using PolySpace Verifier, a commercial software tool that uses algorithms for abstract interpretation, to evaluate its effectiveness and to generate interest in a validation and verification tool.

Between the summers of 2002 and 2003 the team processed modules from NASA's Deep Space 1, a spacecraft that in 1999 flight-tested technologies for future missions, and parts of the 1997 Mars Pathfinder mission and MER.

During a test with 138,000 lines of MPF code the commercial tool returned 80 percent to 85 percent precision, leaving 15 percent to 20 percent to be checked manually. (Consider that when checking the remaining code, 27,600 lines, if each line were a blue line on a sheet of notebook paper, you'd have 9,200 pages of notebook paper to read.) "In a mission, that's still a lot of things you have to verify," Brat said.

Six months later, in June 2003, the team applied CGS to the same MPF code, dropping the processing time dramatically, from 40 hours to 35 minutes -- and boosting precision to 90 percent to 95 percent. Early in July the team ran another test. The program completed the job in about 25 minutes.

The team plans to continue improving the software and is hoping for a role in a future space or planetary exploration mission. Currently, CGS software is built to look for runtime errors in C code, the coding language for the current Mars mission. Next the group will target C++, the programming language that will be adopted for future missions.

In June and July 2003, the twin MER rovers started seven-month journeys from a launch pad at Cape Canaveral Air Force Station in Florida to Mars. The rovers are scheduled to reach separate spots near the martian equator in January 2004. One landing location is in a crater that many scientists believe was once a lake. The other area contains a mineral that on Earth is almost always associated with water.

High hopes rest on MER for a large scientific return, and ultimately for the twin rovers to find evidence that water exists or existed on the red planet. Water is a prerequisite to life as we know it on Earth.

With tools like CGS, automated formal verification can be applied early in the software development process of future Mars missions, catching errors in mission software before the errors become costly or impossible to find and fix. This verification will enable NASA missions with greater reliability and reduced risk.