BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:On Quantitative Software Verification - Marta Kwiatkowska - Oxford
  University
DTSTART:20091111T141500Z
DTEND:20091111T151500Z
UID:TALK19193@talks.cam.ac.uk
CONTACT:Mateja Jamnik
DESCRIPTION:The vast majority of software verification research to date ha
 s concentrated on qualitative analysis methods\, for example the absence o
 f safety violations in program executions. Many programs\, however\, conta
 in randomisation\, timing and resource information. Quantitative verificat
 ion is a technique for establishing quantitative properties of a system mo
 del\, such as the probability of battery power dropping below minimum\, th
 e expected time for message delivery and the expected number of messages l
 ost before protocol termination. Tools such as the probabilistic model che
 cker PRISM (www.prismmodelchecker.org) are widely used in several applicat
 ion domains\, including security and network protocols\, but their applica
 tion to real software is limited.\n\nThis lecture presents recent results 
 concerning quantitative software verification for ANSI-C programs extended
  with random assignment. The goal is to focus on system software that exhi
 bits probabilistic behaviour and properties such as “the maximum probabi
 lity of file-transfer failure”\, or “the maximum expected number of fa
 iled transmissions”. We use a quantitative abstraction-refinement framew
 ork based on predicate abstraction\, in which probabilistic programs are r
 epresented as Markov decision processes and their abstractions as stochast
 ic two-player games. These techniques have been implemented using componen
 ts from GOTO-CC\, SATABS and PRISM and successfully used to verify actual 
 networking software.\n
LOCATION:Lecture Theatre 1\, Computer Laboratory
END:VEVENT
END:VCALENDAR