[Haskell-cafe] ANN: improve-0.0.8

[Tom Hawkins]

ImProve [1] is a imperative programming language for high assurance
applications.  Using Yices [2], ImProve verifies programs will always
adhere to assertion specifications, irrespective of program input.  If
it is possible for an assertion not to be upheld, ImProve will emit a
counter example in the form of a program trace, which illustrates how
the assertion could be violated.

This release improves the means to annotate programs for debugging
(see 'label').  Also, the model checker now includes a pass to remove
irrelevant statements, thus speeding up verification and making
counter example traces easier to read.

At Eaton, we have started using ImProve on critical chunks of code in
our hybrid vehicles.  To date we have ImProve generated C successfully
running in a new prototype vehicle.  In addition to finding a handful
of minor bugs, ImProve has revealed two specification ambiguities
arising from multiple, conflicting requirements.  Due to the nature of
the conflict, it is highly unlikely that the defects would have been
identified with conventional testing.

-Tom

[1] http://hackage.haskell.org/package/improve
[2] http://yices.csl.sri.com/