APAC (APA Checker) is a tool for performing the operations mentioned in the papers on Constraint Markov Chains and Abstract Probabilistic Automata. The tool is implemented in C# 4.0 using the Z3 solver from Microsoft Research for doing quantifier elimination.

At the moment, the tool is in pototype state, but will be extended. To
the best of our knowledge, this is the first implementation effort for
stochastic interfaces

Website: www.cs.aau.dk/~mikkelp/apac