Verification framework for spacecraft control programs targeting the Redfin instruction-set architecture for space satellites subsystems.
The framework is implemented in the Haskell functional programming language and employs a number of GHC language extensions to employ the type system for specification of instruction semantics.
Take a look at the project overview.
The verification framework can be used directly, but for better interaction we also provide a web-browser graphical interface.