seminar zitra v 9:00

[Tomas Bures]

Ahoj,

pripominam, ze zitra je seminar od 9:00.

06/30/10, 09:00
Marta Kwiatkowska (University of Oxford, UK): On Quantitative Software 
Verification
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 and 
successfully used to verify actual networking software.

T.

-- 
Tomas Bures, Ph.D.
Assistant Professor
Department of Distributed and Dependable Systems
Charles University
Malostranske nam.25
11800 Prague 1, Czech Republic
http://dsrg.mff.cuni.cz
Phone: (+420) 2 2191 4236
Fax:   (+420) 2 2191 4323