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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
