Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH scholarly article en Zantema, Hans; Endrullis, Joerg http://www.dagstuhl.de/lipics License
when quoting this document, please refer to the following
DOI:
URN: urn:nbn:de:0030-drops-31381
URL:

;

Proving Equality of Streams Automatically

pdf-format:


Abstract

Streams are infinite sequences over a given data type. A stream specification is a set of equations intended to define a stream. In this paper we focus on equality of streams, more precisely, for a given set of equations two stream terms are said to be equal if they are equal in every model satisfying the given equations. We investigate techniques for proving equality of streams suitable for automation. Apart from techniques that were already available in the tool CIRC from Lucanu and Rosu, we also exploit well-definedness of streams, typically proved by proving productivity. Moreover, our approach does not restrict to behavioral input format and does not require termination. We present a tool Streambox that can prove equality of a wide range of examples fully automatically.

BibTeX - Entry

@InProceedings{zantema_et_al:LIPIcs:2011:3138,
  author =	{Hans Zantema and Joerg Endrullis},
  title =	{{Proving Equality of Streams Automatically}},
  booktitle =	{22nd International Conference on Rewriting Techniques and Applications (RTA'11)},
  pages =	{393--408},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-30-9 },
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{10},
  editor =	{Manfred Schmidt-Schau{\ss}},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2011/3138},
  URN =		{urn:nbn:de:0030-drops-31381},
  doi =		{http://dx.doi.org/10.4230/LIPIcs.RTA.2011.393},
  annote =	{Keywords: streams}
}

Keywords: streams
Seminar: 22nd International Conference on Rewriting Techniques and Applications (RTA'11)
Issue date: 2011
Date of publication: 2011


DROPS-Home | Fulltext Search | Imprint Published by LZI