Proving equality of streams automatically

H. Zantema, J. Endrullis

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

7 Citations (Scopus)
35 Downloads (Pure)

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.
Original languageEnglish
Title of host publicationProceedings of the 22nd International Conference on Rewriting Techniques and Applications (RTA 2011, Novi Sad, Serbia, May 30-June 1, 2011)
EditorsM. Schmidt-Schlauß
Place of PublicationDagstuhl
PublisherSchloss Dagstuhl - Leibniz-Zentrum für Informatik
Pages393-408
ISBN (Print)978-3-939897-30-9
DOIs
Publication statusPublished - 2011

Publication series

NameLIPIcs: Leibniz International Proceedings in Informatics
Volume10
ISSN (Print)1868-8968

Fingerprint Dive into the research topics of 'Proving equality of streams automatically'. Together they form a unique fingerprint.

Cite this