Program

Title: Verifying Concurrent Systems: Logics, Methods and the Problem of Scale
Abstract: Verification and validation methods are important tools for debugging concurrent systems. Much as we need a variety of tools to strengthen a physical structure, we need to deploy multiple formal models, logics
and reasoning methods to reduce bugs in concurrent systems. These methods can be characterized in terms of the scale at which they analyze temporal and spatial properties of a system. I will discuss the advantages and limitations of logics and reasoning methods at different scales–ranging from Statistical Model Checking and Euclidean Model Checking for at probabilistic verification of global behaviors, to decentralized runtime verification and targeted test generation for localized properties.

Title: Automated Methods for Verification of Differential Privacy

Abstract: Differential privacy is a technique developed to preserve individuals’ privacy while performing statistical computations on databases containing private information. The differential privacy framework trades accuracy for privacy. In the framework, a differential privacy mechanism mediates data exchange between the database and data analyst. When the mechanism returns the answer to an analyst’s query, it introduces random noise in the query result before forwarding it to the analyst. Designing correct differential privacy mechanisms is subtle and error-prone, and even relatively minor tweaks to correct mechanisms can lead to loss of privacy. 

In this talk, we present fully automated methods for verifying privacy and accuracy claims of Differential Privacy Mechanisms (DPM). We consider two different methods. In the first method, the DPM of interest is described as a program in a simple programming language that allows constructs for sampling from continuous probability distributions (such as Laplace etc.). In this method, the verification problem is reduced to the problem of checking validity of a formula in a fragment of  first order theory of reals with exponentiation, which is known to be decidable. A tool implementing this technique has been built and employs Mathematica to check the formulas that are generated by the tool. This tool has been used to check the correctness as well as incorrectness of the claims of some well known DPMs presented in the literature. This tool has also been extended to check the accuracy claims of DPMs.

The second method uses an automata model in which some of the DPMs, presented in the literature, can be translated into. We give efficient algorithms, using simple graph algorithms, to check the privacy claims of the DPMs represented in this automata model. We show that this method is sound and complete for DPMs that can be translated into these automata.