Campus Event Calendar
Event Entry
What and Who
Abstraction Methods for Liveness
Amir Pnueli
New York University and Weizmann Institute (Emeritus)
Virtual Seminar
AG 1, RG1
AG Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Tuesday, 25 November 2008
17:00
60 Minutes
E1 4
007
Saarbrücken
Abstract
It is a known fact that finitary state abstraction methods, such as
predicate abstraction, are inadequate for verifying general liveness
properties or even termination of sequential programs. In this talk we
will present an abstraction approach called "ranking abstraction"
which is sound and complete for verifying all temporally specified
properties, including all liveness properties.
We will start by presenting a general simple framework for state
abstraction emphasizing that, in order to get soundness, it is
necessary to apply an over-approximating abstraction to the system and
an under-approximating abstraction to the (temporal) property. We show
that finitary version of this abstraction are complete for verifying
all safety properties.
We then consider abstraction approaches to the verification of
deadlock freedom, presenting some sufficient conditions guaranteeing
that deadlock freedom is inherited from the concrete to the abstract.
Finally, we introduce the method of ranking abstraction and illustrate
its application to the verification of termination and more general
liveness properties. In this presentation we emphasize the similarity
between predicate abstraction and its extension into ranking
abstraction. In particular, we illustrate how abstraction refinement
can be applied to ranking abstraction. Time permitting, we will
present a brief comparison between ranking abstraction and the
methods of transition abstraction developed by Podelski,
Rybalchenko, and Cook which underly the "Terminator" system.
predicate abstraction, are inadequate for verifying general liveness
properties or even termination of sequential programs. In this talk we
will present an abstraction approach called "ranking abstraction"
which is sound and complete for verifying all temporally specified
properties, including all liveness properties.
We will start by presenting a general simple framework for state
abstraction emphasizing that, in order to get soundness, it is
necessary to apply an over-approximating abstraction to the system and
an under-approximating abstraction to the (temporal) property. We show
that finitary version of this abstraction are complete for verifying
all safety properties.
We then consider abstraction approaches to the verification of
deadlock freedom, presenting some sufficient conditions guaranteeing
that deadlock freedom is inherited from the concrete to the abstract.
Finally, we introduce the method of ranking abstraction and illustrate
its application to the verification of termination and more general
liveness properties. In this presentation we emphasize the similarity
between predicate abstraction and its extension into ranking
abstraction. In particular, we illustrate how abstraction refinement
can be applied to ranking abstraction. Time permitting, we will
present a brief comparison between ranking abstraction and the
methods of transition abstraction developed by Podelski,
Rybalchenko, and Cook which underly the "Terminator" system.
Contact
Jennifer Müller
900
--email hidden
passcode not visible
logged in users only
Jennifer Müller, 11/19/2008 15:33 -- Created document.