Max-Planck-Institut für Informatik
max planck institut
informatik
mpii logo Minerva of the Max Planck Society
 

MPI-INF or MPI-SWS or Local Campus Event Calendar

<< Previous Entry Next Entry >> New Event Entry Edit this Entry Login to DB (to update, delete)
What and Who
Title:Randomized Algorithms Meets Formal Verification
Speaker:Justin Hsu
coming from:University of Pennsylvania
Speakers Bio:Justin Hsu is a final year graduate student in Computer Science at the University of Pennsylvania. He obtained his undergraduate degree in Mathematics

from Stanford University. His research interests span formal verification and theoretical computer science, including verification of randomized algorithms,
differential privacy, and game theory. He is the recipient of a Simons graduate fellowship in Theoretical Computer Science.

Event Type:SWS Colloquium
Visibility:SWS, RG1, MMCI
We use this to send out email in the morning.
Level:AG Audience
Language:English
Date, Time and Location
Date:Wednesday, 8 March 2017
Time:10:00
Duration:90 Minutes
Location:Saarbr├╝cken
Building:E1 5
Room:029
Abstract
Algorithms and formal verification are two classical areas of computer science. The two fields apply rigorous mathematical proof to seemingly disparate ends---on the one hand, analyzing computational efficiency of algorithms; on the other, designing techniques to mechanically show that programs are correct.

In this talk, I will present a surprising confluence of ideas from these two areas. First, I will show how coupling proofs, used to analyze random walks and Markov chains, correspond to proofs in the program logic pRHL (probabilistic Relational Hoare Logic). This connection enables formal verification of novel probabilistic properties, and provides an structured understanding of proofs by coupling. Then, I will show how an approximate version of pRHL, called apRHL, points to a new, approximate version of couplings closely related to differential privacy. The corresponding proof technique---proof by approximate coupling---enables cleaner proofs of differential privacy, both for humans and for formal verification. Finally, I will share some directions towards a possible "Theory AB", blending ideas from both worlds.
Contact
Name(s):Claudia Richter
Phone:9303 9103
EMail:--email address not disclosed on the web
Video Broadcast
Video Broadcast:YesTo Location:Kaiserslautern
To Building:G26To Room:111
Meeting ID:
Tags, Category, Keywords and additional notes
Note:
Attachments, File(s):

Created:
Claudia Richter/MPI-SWS, 02/10/2017 11:03 AM
Last modified:
Uwe Brahm/MPII/DE, 03/08/2017 07:01 AM
  • Uwe Brahm, 03/06/2017 05:31 PM
  • Claudia Richter, 02/10/2017 11:09 AM -- Created document.