salle A. Turing CE4
31 May 2012 - 14h00
Quantitative Abstraction Refinement
by Pavol Cerny from IST Austria
Abstract: We propose a general framework for abstraction with respect to
quantitative properties of systems, such as worst-case execution time
(WCET) or power consumption. Our framework provides a systematic way
for counter-example guided abstraction refinement (CEGAR) for
quantitative properties. The salient aspect of the framework is that
it allows anytime verification, that is, verification algorithms
that can be stopped at any time (for example, due to exhaustion of
memory) and report approximations that improve monotonically when the
algorithms are given more time. We define a number of quantitative
abstraction and refinement schemes, which differ in terms of how much
quantitative information they keep from the original system. We study
the properties of these abstractions; in particular, we give
conditions that define classes of quantitative properties for which
the abstractions provide overapproximations. We also present
algorithms for the evaluation of quantitative properties on the
abstract systems. We perform a case study to evaluate both the anytime
verification aspect and the trade-offs offered by various quantitative
abstractions. The case study uses refinements of cache abstraction to
obtain overapproximations for the WCET analysis of executables.
This is joint work with Thomas Henzinger and Arjun Radhakrishna.
Pavol Cerny a été classé 1er au concours CR2 du CNRS, il est susceptible d'être affecté à Verimag.
