BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Automated Analysis of Probabilistic Programs - Joost-Pieter Katoen
 \, RWTH Aachen
DTSTART:20130718T130000Z
DTEND:20130718T140000Z
UID:TALK46221@talks.cam.ac.uk
CONTACT:Microsoft Research Cambridge Talks Admins
DESCRIPTION:Probabilistic programs are pivotal for cryptography\, privacy 
 and quantum programs\, are typically a few number of lines\, but hard to u
 nderstand and analyse.  The main challenge for their automated analysis is
  the infinite domain of the program variables combined with the occurrence
  of parameters.  Here\, parameters can range over concrete probabilities b
 ut can also encompass various aspects of the program\, such as number of p
 articipants\, size of certain variables etc.\n\nMcIver and Morgan have ext
 ended the seminal proof method of Floyd and Hoare for sequential programs 
 to probabilistic programs by making the program annotations real- rather t
 han Boolean-valued expressions in the program variables.  As in traditiona
 l program analysis\, the crucial annotations are the loop invariants.  The
  problem to synthesize loop invariants is very challenging for probabilist
 ic programs where real-valued\, quantitative invariants are needed.\n\nIn 
 this talk\, we present a novel approach to synthesize loop invariants for 
 the class of linear probabilistic programs. In order to provide an operati
 onal interpretation to the quantitative program annotations\, we give a si
 mple operational semantics using parameterized infinite-state Markov decis
 ion processes and prove its connection to McIver's and Morgan's wp-semanti
 cs.  Finally\, we show some of the internals of the prototypical tool PRIN
 SYS supporting our invariant-generation approach.\n\n
LOCATION:Auditorium\, Microsoft Research Ltd\, 21 Station Road\, Cambridge
 \, CB1 2FB
END:VEVENT
END:VCALENDAR