IMITATOR is a parametric timed model checker taking as input extensions of parametric timed automata, and synthesizing parameter valuations for safety properties and more.

EMPHASIS: An Emotional Phoneme-based Acoustic Model for Speech Synthesis System

InSPEqTor (INference of Shortest Paths with EQuivalent abstracT behaviOR) is a prototype implementation to compute parameter valuations in parametric directed weighted graphs such that shortest paths are preserved.

ImpRator (Inverse Method for Policy with Reward AbstracT behaviOR) is a prototype implementation to compute parameter valuations in parametric Markov decision processes such that optimal policies remain optimal.