Campus Event Calendar
Event Entry
What and Who
Automating Proofs of Relational Properties of Probabilistic Programs
Prof. Dr. Andrey Rybalchenko
Microsoft Research
CISPA Distinguished Lecture Series
AG 1, AG 2, AG 3, AG 4, AG 5, SWS, RG1, MMCI
Expert Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Wednesday, 23 April 2014
13:30
60 Minutes
E1 5
002
Saarbrücken
Abstract
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
Joint work with Klaus v. Gleissenthall and Santiago Zanella-Beguelin
Contact
Stephanie Feyahn
0681-302 71922
--email hidden
passcode not visible
logged in users only
Tags, Category, Keywords and additional notes
CISPA; Distinguished Lecture; Michael Backes
Stephanie Feyahn, 04/09/2014 10:42 -- Created document.