Additional Projects

• Predicate monads, a compositional verification framework for monadic programs
• Specware-Coq is a plugin for Coq that allows synthesis of correct-by-construction software from high-level specifications