76 citations · 182 across the 15 of their papers we have counts for
16 papers
Forward and Backward Simulations for Partially Observable Probability
Chris Chen, Annabelle McIver, Carroll Morgan
Data refinement is the standard extension of a refinement relation from programs to datatypes (i.e. a behavioural subtyping relation). Forward/backward simulations provide a tracta…
Source-level reasoning for quantitative information flow
Chris Chen, Annabelle McIver, Carroll Morgan
We present a novel formal system for proving quantitative-leakage properties of programs. Based on a theory of Quantitative Information Flow (QIF) that models information leakage a…
A novel analysis of utility in privacy pipelines, using Kronecker products and quantitative information flow
Mário S. Alvim, Natasha Fernandes, Annabelle McIver +2
We combine Kronecker products, and quantitative information flow, to give a novel formal analysis for the fine-grained verification of utility in complex privacy pipelines. The com…
Flexible and scalable privacy assessment for very large datasets, with an application to official governmental microdata
Mário S. Alvim, Natasha Fernandes, Annabelle McIver +2
We present a systematic refactoring of the conventional treatment of privacy analyses, basing it on mathematical concepts from the framework of Quantitative Information Flow (QIF).…
The Laplace Mechanism has optimal utility for differential privacy over continuous queries
Natasha Fernandes, Annabelle McIver, Carroll Morgan
Differential Privacy protects individuals' data when statistical queries are published from aggregated databases: applying "obfuscating" mechanisms to the query results makes the r…
Correctness by construction for probabilistic programs
Annabelle McIver, Carroll Morgan
The "correct by construction" paradigm is an important component of modern Formal Methods, and here we use the probabilistic Guarded-Command Language to illustrate…