Coupled Relational Symbolic Execution

by Marco Gaboardi

• When: Friday, 05/03/2021, between 2pm and 3pm EST (7pm - 8pm UTC)
• Where: Zoom; Outside guests please RSVP by emailing Harley Eades
• YouTube Recording: https://youtu.be/0f-srpBeXAI

Abstract

Symbolic execution is a classic technique used for testing, counterexample generation and to prove absence of bugs. Here we will present an extension of symbolic execution to support these tasks specifically for probabilistic relational properties, that is properties expressed in terms of two runs of a probabilistic program. Our technique leverages two ideas: relational reasoning and probabilistic coupling. These ideas have been used for formal verification using program logics and type systems. We show here how they can also be smoothly integrated with symbolic execution in order to support verification and finding violations to probabilistic relational properties. To guide our development and presentation, we will focus on differential privacy, an important example of probabilistic relational property which has been studied extensively in recent work.

The talk will be based on joint work with Gian Pietro Farina (as part of his PhD at the University at Buffalo, SUNY) and Stephen Chong (Harvard University).