PRINSYS – PRobabilistic INvariant SYnthesiS


PRINSYS is a tool for invariant generation for probabilistic programs. It takes a constraint-based approach and relies on quantifier elimination techniques to obtain the results. PRINSYS is under constant development so check back for news soon!
Below you will find short download instructions and a quick manual to get started.
If you have any questions or suggestions, do not hesitate to contact: Friedrich Gretz (fgretz at cs dot

For further information and download options see