On Quantitative Software Verification

Duration: 53 mins 26 secs

Share this media item:

Embed this media item:

<iframe width="_width_" height="_height_" src="https://sms.cam.ac.uk/media/852573/embed" frameborder="0" scrolling="no" allowfullscreen></iframe>

Choose size:

About this item

Available Formats

About this item

Description:	http://www.talks.cam.ac.uk/talk/index/19193


Created:	2010-06-10 12:25
Collection:	Computer Laboratory Wednesday Seminars
Publisher:	University of Cambridge
Copyright:	Computer Laboratory
Language:	eng (English)


Abstract:	The vast majority of software verification research to date has concentrated on qualitative analysis methods, for example the absence of safety violations in program executions. Many programs, however, contain randomisation, timing and resource information. Quantitative verification is a technique for establishing quantitative properties of a system model, such as the probability of battery power dropping below minimum, the expected time for message delivery and the expected number of messages lost before protocol termination. Tools such as the probabilistic model checker PRISM (www.prismmodelchecker.org) are widely used in several application domains, including security and network protocols, but their application to real software is limited. This 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 exhibits probabilistic behaviour and properties such as “the maximum probability of file-transfer failure”, or “the maximum expected number of failed transmissions”. We use a quantitative abstraction-refinement framework based on predicate abstraction, in which probabilistic programs are represented as Markov decision processes and their abstractions as stochastic two-player games. These techniques have been implemented using components from GOTO -CC, SATABS and PRISM and successfully used to verify actual networking software.

Abstract:

The vast majority of software verification research to date has concentrated on qualitative analysis methods, for example the absence of safety violations in program executions. Many programs, however, contain randomisation, timing and resource information. Quantitative verification is a technique for establishing quantitative properties of a system model, such as the probability of battery power dropping below minimum, the expected time for message delivery and the expected number of messages lost before protocol termination. Tools such as the probabilistic model checker PRISM (www.prismmodelchecker.org) are widely used in several application domains, including security and network protocols, but their application to real software is limited.

This 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 exhibits probabilistic behaviour and properties such as “the maximum probability of file-transfer failure”, or “the maximum expected number of failed transmissions”. We use a quantitative abstraction-refinement framework based on predicate abstraction, in which probabilistic programs are represented as Markov decision processes and their abstractions as stochastic two-player games. These techniques have been implemented using components from GOTO -CC, SATABS and PRISM and successfully used to verify actual networking software.

Available Formats

Format	Quality	Bitrate	Size
MPEG-4 Video	480x360	1.84 Mbits/sec	738.79 MB	View	Download
WebM	480x360	656.49 kbits/sec	257.01 MB	View	Download
Flash Video	480x360	806.1 kbits/sec	315.97 MB	View	Download
Flash Video	320x240	438.21 kbits/sec	171.77 MB	View	Download
iPod Video	480x360	505.15 kbits/sec	198.00 MB	View	Download
MP3	44100 Hz	125.03 kbits/sec	48.80 MB	Listen	Download
Auto *	(Allows browser to choose a format it supports)