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 is ongoing work. The tool is written in Haskell.

HyperPAYNT

A tool for synthesizing controllers for Markov Decision Processes against probabilistic hyperproperty specifications. It is an extension of PAYNT, and uses STORM as underlying model checker. The tool is written in Python.