Sciweavers

FROCOS
2005
Springer

Proving Liveness with Fairness Using Rewriting

14 years 5 months ago
Proving Liveness with Fairness Using Rewriting
Abstract. In this paper we combine rewriting techniques with verification issues. More precisely, we show how techniques for proving relative termination of term rewrite systems (TRSs) can be applied to prove liveness properties in fair computations. We do this using a new transformation which is stronger than the sound transformation from [5] but still is suitable for automation. On the one hand we show completeness of this approach under some mild conditions. On the other hand we show how this approach applies to some examples completely automatically, using the TPA tool designed for proving relative termination of TRSs. In particular we succeed in proving liveness in the classical readers-writers synchronization problem.
Adam Koprowski, Hans Zantema
Added 27 Jun 2010
Updated 27 Jun 2010
Type Conference
Year 2005
Where FROCOS
Authors Adam Koprowski, Hans Zantema
Comments (0)