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/