@hackage improve0.0.5

An imperative, verifiable programming language for high assurance applications.

ImProve is an imperative DSL intended for high assurance, embedded applications. ImProve uses infinite state, unbounded model checking to verify programs adhere to specifications, which are written in the form of assertion statements. Yices (required) is the backend SMT solver.