Tools

POMC

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 programming language, MiniProc, and specifications expressed in the logic POTL (standing for Precedence Oriented Temporal Logic). An extension for probabilistic recursive programs (POPACheck) is ongoing work. The tool is written in Haskell.

HyperPAYNT / PHSynt

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.