| 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
(Giesl, Zantema, 2003) 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.
Proving Liveness with Fairness using Rewriting
In
Proceedings of the 5th International Workshop on Frontiers of Combining Systems
( FroCoS '05),
Vienna, Austria.
BibTeX:@inproceedings{livfair-FROCOS-05,
author = {Adam Koprowski and Hans Zantema},
title = {Proving Liveness with Fairness using Rewriting},
booktitle = {Proceedings of the 5th International Workshop on Frontiers of Combining Systems (FroCoS '05)},
year = {2005},
series = {Lecture Notes in Computer Science},
volume = {3717},
pages = {232--247},
} | 
