[Haskell-cafe] ANN: improve-0.2.2

[Tom Hawkins]

ImProve [1] is an imperative DSL for high assurance, embedded
applications.  This release includes a new compositional proof
framework where users can leverage previously proved theorems to aid
the proof of new theorems.  This new addition was inspired from
discussions with Lee Pike [2].

Lee also recommended the strategy of building disjunctive invariants
to reduce, if not eliminate the need for multi step induction, thus
dramatically reducing proof time.  Using these new strategies with
ImProve, we where able to verify several realtime safety properties of
an Eaton Hybrid Hydraulic program.

-Tom

[1] http://hackage.haskell.org/package/improve
[2] http://groups.google.com/group/fp-embedded/browse_thread/thread/63cd023e8f17b613?hl=en