Campus Event Calendar
Event Entry
What and Who
Verifying Probabilistic Programs
Stefan Kiefer
University of Oxford
SWS Colloquium
AG 1, AG 2, AG 3, AG 4, AG 5, SWS, RG1, MMCI
AG Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Monday, 16 December 2013
11:00
60 Minutes
G26
113
Kaiserslautern
Abstract
I am going to talk about two approaches to the verification of probabilistic systems: (1) equivalence analysis; and (2) termination analysis.
Deciding equivalence of probabilistic automata is a key problem for establishing various behavioural and anonymity properties of probabilistic systems. In particular, it is at the heart of the tool APEX, an analyser for probabilistic programs. APEX is based on game semantics and analyses a broad range of anonymity and termination properties of randomised protocols and other open programs.
Proving programs terminating is a fundamental computer science challenge. Recent research has produced powerful tools that can check a wide range of programs for termination. The analogue for probabilistic programs, namely termination with probability one (``almost-sure termination''), is an equally important property for randomised algorithms and probabilistic protocols. We have developed a novel algorithm for proving almost-sure termination of probabilistic programs. Our algorithm exploits the power of state-of-the-art model checkers and termination provers for nonprobabilistic programs.
Deciding equivalence of probabilistic automata is a key problem for establishing various behavioural and anonymity properties of probabilistic systems. In particular, it is at the heart of the tool APEX, an analyser for probabilistic programs. APEX is based on game semantics and analyses a broad range of anonymity and termination properties of randomised protocols and other open programs.
Proving programs terminating is a fundamental computer science challenge. Recent research has produced powerful tools that can check a wide range of programs for termination. The analogue for probabilistic programs, namely termination with probability one (``almost-sure termination''), is an equally important property for randomised algorithms and probabilistic protocols. We have developed a novel algorithm for proving almost-sure termination of probabilistic programs. Our algorithm exploits the power of state-of-the-art model checkers and termination provers for nonprobabilistic programs.
Contact
Rupak Majumdar
--email hidden
Video Broadcast
Yes
Saarbrücken
E1 5
029
passcode not visible
logged in users only
Susanne Girard, 12/09/2013 13:59 -- Created document.