We learned this week of ImProve, a lightweight DSL intended for building high assurance embedded applications. Developed by Tom Hawkins, the tool is an EDSL that performs formal verification (via. model checking) and code generation. The host language is Haskell; meaning ImProve programs are nothing more than Haskell programs that call the ImProve library API.
ImProve’s semantics are extremely simple:
-
- It is an imperative language like C or Ada.
-
- It only has 3 datatypes (bool, int, float).
-
- There are a total of 16 expression types (add, subtract, AND, OR, etc.).
-
- Statements consist of variables assignments, conditional “IF” statements, and assertions.
In terms of the ImProve compiler structure, a thin layer of Haskell helps translate ImProve programs down to an intermediate representation, from which programs are verified and C code is generated.
For verification, the IR language is passed to a k-induction model checker (part of the ImProve library), which makes calls down to an SMT solver (currently Yices). ImProve provides assertions statements to capture design intent. Assertions can be seeded with previously proven lemmas to aid verification convergence.
For more information, please visit the project website:
https://github.com/tomahawkins/improve/wiki/ImProve