WALi and OpenNWA news

Jan. 31, 2012

We are now releasing the release candidate of WALi 4.0! Included with the WALi distribution is the first public release of a new library, OpenNWA. OpenNWA provides an implementation of nested-word automata, and interoperates tightly with WALi. More information about both libraries is available to the left, as well as the download page.

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.”