WALi and OpenNWA news

Aug 27, 2012

The release version of WALi/OpenNWA 4.1 is now available for download. There are only minor changes from the RC1. [download]

July 30, 2012

We are now releasing the release candidate of WALi/OpenNWA 4.1! This contains several efficiency improvements relative to 4.0, mostly in terms of OpenNWA. (See the CHANGES file in the distribution.) [download]

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