[Haskell-cafe] ANN: improve-0.2.2

Tom Hawkins tomahawkins at gmail.com
Sun Dec 12 16:46:34 CET 2010

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.


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

More information about the Haskell-Cafe mailing list