Abstract
I will describe our recent efforts in automatically verifying correctness and accuracy of differentially private algorithms. I will show how traditional techniques from logic-based software verification can be extended to the probabilistic setting, by synthesizing appropriate axiomatizations of the probabilistic semantics. The result is a powerful technique that can automatically prove the correctness and accuracy of sophisticated algorithms from the differential privacy literature.