Campus Event Calendar
Event Entry
What and Who
Completeness Results for Predicate Abstraction with Refinement
Rayna Dimitrova
MPII
Masters Seminar
AG 1, AG 2, AG 3, AG 4, AG 5
MPI Audience
Note: We use this to send email in the morning.
Date, Time and Location
Tuesday, 29 November 2005
13:00
60 Minutes
46.1 - MPII
0.24
Saarbrücken
Abstract
The verification of programs is undecidable in general. In practice,
semi-algorithms that may not terminate on some inputs are used. It is
worth identifying sufficient conditions for when the semi-algorithm is
guaranteed to terminate and thus amounts to a decision procedure for the
verification problem for a restricted class of programs.
I will present predicate abstraction with abstraction refinement, which
is one approach to verifying properties of infinite-state systems. We know
that it is complete for systems that are equivalent(formally: bisimilar)
to finite-state systems(finite-state means: each program variable can have
only finitely many values). For a more general class, the one of
well-structured transition systems, the coverability problem is known to be
decidable. I address the question of completeness of predicate abstraction
with refinement for checking safety properties of such systems.
semi-algorithms that may not terminate on some inputs are used. It is
worth identifying sufficient conditions for when the semi-algorithm is
guaranteed to terminate and thus amounts to a decision procedure for the
verification problem for a restricted class of programs.
I will present predicate abstraction with abstraction refinement, which
is one approach to verifying properties of infinite-state systems. We know
that it is complete for systems that are equivalent(formally: bisimilar)
to finite-state systems(finite-state means: each program variable can have
only finitely many values). For a more general class, the one of
well-structured transition systems, the coverability problem is known to be
decidable. I address the question of completeness of predicate abstraction
with refinement for checking safety properties of such systems.
Contact
Kerstin Meyer-Ross
9325-226
--email hidden
passcode not visible
logged in users only
Friederike Gerndt, 11/23/2005 11:33 -- Created document.