ImProve

ImProve is a lightweight DSL intended for building high assurance embedded applications. ImProve is a simple imperative language with variable assignments and conditional statements. ImProve assertions are formally verified using SMT model checking. For implementation and system simulation, ImProve compiles to C, Ada, Simulink, and Modelica.

The ImProve compiler and language are implemented in Haskell.

Getting Started

• Download the Haskell Platform.
• Download the Yices SMT Solver.
• Install the ImProve library from Hackage:

$ cabal update
$ cabal install improve

Tutorials

• Hello World: A simple first program with code generation.
• Language Overview: A tour of ImProve's language types and constructs.
• Control Laws: Examples of feedback control laws and DSP in ImProve.
• State Machines: Examples of building state machines and statecharts in ImProve.
• Verification Primer: An overview of k-induction model checking with ImProve.
• Invariant Strengthening: Using invariants to aid verification.