News

Oct. 1, 2009

WALi was used as the analysis engine in a tool created by Rubio-Gonzalez et al. [link], which analyzes error propagation in file-systems code. Besides finding . . . summarize their results, a la Cindy's slides, on bugs found and the false-positive rate . . ., the tool was also used at the NASA/JPL Laboratory for Reliable Software to check code in the Mars Science Laboratory. To date, the tool has found one error-propagation bug in “flying” code (code used for space missions):

“We've found one legitimate problem. [...] We call a non-void function (that can return some critical error codes) and don't assign the return value, dropping some nice things such as EASSERT, EABOUND, and EEBADHDR on the ground. We would have expected the compiler or [another code-checking tool] to catch that, actually.”