Max-Planck-Institut für Informatik
max planck institut
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:Automating Proofs of Relational Properties of Probabilistic Programs
Speaker:Prof. Dr. Andrey Rybalchenko
coming from:Microsoft Research
Speakers Bio:
Event Type:CISPA Distinguished Lecture Series
Visibility:D1, D2, D3, D4, D5, SWS, RG1, MMCI
We use this to send out email in the morning.
Level:Expert Audience
Date, Time and Location
Date:Wednesday, 23 April 2014
Duration:60 Minutes
Building:E1 5
Some security properties go beyond what is expressible in terms of an individual execution of a single program. In particular, many security policies in cryptography can be naturally phrased as relational properties of two open probabilistic programs. Writing and verifying proofs of such properties is an error-prone task that calls for automation and tool support. One of the main difficulties in automating these proofs lies in finding adequate relational invariants for loops and specifications for program holes. In this paper we show how to automate proofs of relational properties of open probabilistic programs by adapting techniques for the automatic generation of universally quantified invariants in a non-relational setting.

Joint work with Klaus v. Gleissenthall and Santiago Zanella-Beguelin
Name(s):Stephanie Feyahn
Phone:0681-302 71922
EMail:--email address not disclosed on the web
Video Broadcast
Video Broadcast:NoTo Location:
Tags, Category, Keywords and additional notes
Keywords:CISPA; Distinguished Lecture; Michael Backes
Attachments, File(s):
  • Stephanie Feyahn, 04/09/2014 10:42 AM -- Created document.