Campus Event Calendar
Event Entry
What and Who
Transition Predicate Abstraction and Fair Termination
Andrey Rybalchenko
Ringvorlesung
AG 1, AG 2, AG 3, AG 4, AG 5
AG Audience
Note: We use this to send email in the morning.
Date, Time and Location
Thursday, 16 December 2004
13:00
-- Not specified --
45
016
Saarbrücken
Abstract
Predicate abstraction is the basis of many program verification tools.
Until now, the only known way to overcome the inherent limitation of
predicate abstraction to safety properties was to manually
annotate the finite-state abstraction of a program. We extend
predicate abstraction to transition predicate abstraction.
Transition predicate abstraction goes beyond the idea of finite
abstract-state programs (and checking the absence of loops).
Instead, our abstraction algorithm transforms a program into a
finite abstract-transition program. Then, a second algorithm
checks fair termination. The two algorithms together yield an
automated method for the verification of liveness properties under
full fairness assumptions (justice and compassion). In summary, we
exhibit principles that extend the applicability of predicate
abstraction-based program verification to the full set of temporal
properties.
Until now, the only known way to overcome the inherent limitation of
predicate abstraction to safety properties was to manually
annotate the finite-state abstraction of a program. We extend
predicate abstraction to transition predicate abstraction.
Transition predicate abstraction goes beyond the idea of finite
abstract-state programs (and checking the absence of loops).
Instead, our abstraction algorithm transforms a program into a
finite abstract-transition program. Then, a second algorithm
checks fair termination. The two algorithms together yield an
automated method for the verification of liveness properties under
full fairness assumptions (justice and compassion). In summary, we
exhibit principles that extend the applicability of predicate
abstraction-based program verification to the full set of temporal
properties.
Contact
--email hidden
passcode not visible
logged in users only
Bahareh Kadkhodazadeh, 12/13/2004 11:19
Bahareh Kadkhodazadeh, 10/21/2004 12:46 -- Created document.
Bahareh Kadkhodazadeh, 10/21/2004 12:46 -- Created document.