The Precedence Oriented Model Checker is a model checker for recursive procedural programs and context-free properties such as pre/post conditions and exception safety. It supports a custom domain-specific programming language, MiniProc, and specifications expressed in the logic POTL (standing for Precedence Oriented Temporal Logic). The tool is written in Haskell.
An extension of POMC towards the verification of probabilistic recursive programs. It support a custom domain-specific programming language, MiniProb, and specifications in LTL and a fragment of POTL. The extension is written in Haskell as well.
Two tools for synthesizing controllers for Markov Decision Processes against probabilistic hyperproperty specifications. They are extensions of PAYNT, and use a customized version of STORM as underlying model checker. The tools are written in Python.