ImProve [1] is an imperative DSL for hard realtime embedded applications. ImProve programs are verified with infinite state,unbounded model checking (k-induction, invariant strengthening, SMT). In addition to C, ImProve now supports Simulink [2] as a backend target. Simulink is a popular language for automotive and aerospace control systems.
-Tom [1] http://hackage.haskell.org/package/improve [2] http://www.mathworks.com/ _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
