Proving liveness with fairness using rewriting

A. Koprowski, H. Zantema

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureConferentiebijdrageAcademicpeer review

5 Citaten (Scopus)

Samenvatting

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.
Originele taal-2Engels
TitelFrontiers of Combining Systems (Proceedings 5th International Workshop, FroCoS 2005, Vienna, Austria, September 19-21, 2005)
RedacteurenB. Gramlich
Plaats van productieBerlin
UitgeverijSpringer
Hoofdstuk13
Pagina's232-247
Aantal pagina's16
ISBN van elektronische versie978-3-540-31730-2
ISBN van geprinte versie3-540-29051-6, 978-3-540-29051-3
DOI's
StatusGepubliceerd - 2005

Publicatie series

NaamLecture Notes in Computer Science (LNCS)
Volume3717
ISSN van geprinte versie0302-9743
NaamLecture Notes in Artificial Intelligence (LNAI)
Volume3717

Vingerafdruk

Duik in de onderzoeksthema's van 'Proving liveness with fairness using rewriting'. Samen vormen ze een unieke vingerafdruk.

Citeer dit