In this tool, the branching time temporal logic dpCTL is developed for specifying differential privacy. Several differentially private mechanisms are formalized as Markov chains or Markov decision processes. Using formal models, subtle privacy conditions are specified by dpCTL. In order to verify privacy properties automatically, model checking problems are investigated. We give and implement a model checking algorithm for Markov chains and for MDPs, it's shown to be undecidable. For more information about the tool and the logic dpCTL, please refer to this paper:

Liu D., Wang BY., Zhang L. (2018) Model Checking Differentially Private Properties. In: Ryu S. (eds) Programming Languages and Systems. APLAS 2018. Lecture Notes in Computer Science, vol 11275. Springer, Cham. https://doi.org/10.1007/978-3-030-02768-1_21