DPO-SYNT: Discrete control SYNThesis for Partially-Observed systems
It is a C based software toolbox developed by University of Michigan Discrete Event Systems Group. It is designed to solve a class of property-enforcement synthesis problems for partially-observed discrete event systems. [current version].
VEiP: Verification and Enforcement using Insertion for Opacity
VEiP is a Java based toolbox developed by by University of Michigan Discrete Event Systems Group. It is designed for verification and enforcement of opacity properties formulated in discrete event systems. [current version].
EdiSyn: Edit Function Synthesis for Opacity Enforcement
EdiSyn is a Python-based toolkit developed by University of Michigan Discrete Event Systems Group. It is designed for synthesizing obfuscators that enforce privacy while preserving utility with formal guarantees. It uses the BDD library CUDD via the Python package dd to implement the algorithms symbolically. [current version].