Proving that programs are differentially private

Annabelle McIver*, Carroll Morgan

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference proceeding contributionpeer-review

1 Citation (Scopus)


We extend recent work in Quantitative Information Flow (QIF) to provide tools for the analysis of programs that aim to implement differentially private mechanisms. We demonstrate how differential privacy can be expressed using loss functions, and how to use this idea in conjunction with a QIF-enabled program semantics to verify differentially private guarantees. Finally we describe how to use this approach experimentally using Kuifje, a recently developed tool for analysing information-flow properties of programs.

Original languageEnglish
Title of host publicationProgramming Languages and Systems
Subtitle of host publication17th Asian Symposium, APLAS 2019, Proceedings
EditorsAnthony Widjaja Lin
Place of PublicationCham
PublisherSpringer, Springer Nature
Number of pages16
ISBN (Electronic)9783030341756
ISBN (Print)9783030341749
Publication statusPublished - 1 Jan 2019
Event17th Asian Symposium on Programming Languages and Systems, APLAS 2019 - Bali, Indonesia
Duration: 1 Dec 20194 Dec 2019

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume11893 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference17th Asian Symposium on Programming Languages and Systems, APLAS 2019
City Bali


  • Differential privacy
  • privacy
  • Probabilistic program semantics
  • Quantitative Information Flow
  • verification


Dive into the research topics of 'Proving that programs are differentially private'. Together they form a unique fingerprint.

Cite this