Formal methods provide tools for helping program developers to design their programs and to guarantee them correct. Different applications have different requirements in term of support that they have to provide to developers and in terms of notions of correctness that they have to provide. In this mini-course I will introduce participants to some of the requirements of differential privacy applications and how formal methods address them.

The mini-course will be divided in three parts. In the first part, I will give an overview of some of the systems, and the problem they address, that have been proposed to support program developers in designing differential privacy applications. In the second part, I will motivate through examples a formal method that we used to verify differentially private applications. Finally, in the third and last part of the mini-course, I will present some recent extensions and alternatives to the formal method presented in the second part and discuss where the community working on these topics is heading.