A tool proving well-definedness of streams using termination tools

H. Zantema

doi:10.1007/978-3-642-03741-2_32

A tool proving well-definedness of streams using termination tools

H. Zantema

Formal System Analysis

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

3 Citations (Scopus)

2 Downloads (Pure)

Abstract

A stream specification is a set of equations intended to define a stream, that is, an infinite sequence over a given data type. In [5] a transformation from such a stream specification to a TRS is defined in such a way that termination of the resulting TRS implies that the stream specification admits a unique solution. In this tool description we present how proving such well-definedness of several interesting boolean stream specifications can be done fully automatically using present powerful tools for proving TRS termination.

Original language	English
Title of host publication	Algebra and Coalgebra in Computer Science (Third International Conference, CALCO 2009, Udine, Italy, September 7-10, 2009. Proceedings)
Editors	A. Kurz, M. Lenisa, A. Tarlecki
Place of Publication	Berlin
Publisher	Springer
Pages	449-456
ISBN (Print)	978-3-642-03740-5
DOIs	https://doi.org/10.1007/978-3-642-03741-2_32
Publication status	Published - 2009

Publication series

Name	Lecture Notes in Computer Science
Volume	5728
ISSN (Print)	0302-9743

Access to Document

10.1007/978-3-642-03741-2_32

Fingerprint Dive into the research topics of 'A tool proving well-definedness of streams using termination tools'. Together they form a unique fingerprint.

Cite this

Zantema, H. (2009). A tool proving well-definedness of streams using termination tools. In A. Kurz, M. Lenisa, & A. Tarlecki (Eds.), Algebra and Coalgebra in Computer Science (Third International Conference, CALCO 2009, Udine, Italy, September 7-10, 2009. Proceedings) (pp. 449-456). (Lecture Notes in Computer Science; Vol. 5728). Springer. https://doi.org/10.1007/978-3-642-03741-2_32

@inproceedings{2f70fdf2b5f84a6e8388310e8c4cde13,

title = "A tool proving well-definedness of streams using termination tools",

abstract = "A stream specification is a set of equations intended to define a stream, that is, an infinite sequence over a given data type. In [5] a transformation from such a stream specification to a TRS is defined in such a way that termination of the resulting TRS implies that the stream specification admits a unique solution. In this tool description we present how proving such well-definedness of several interesting boolean stream specifications can be done fully automatically using present powerful tools for proving TRS termination.",

author = "H. Zantema",

year = "2009",

doi = "10.1007/978-3-642-03741-2_32",

language = "English",

isbn = "978-3-642-03740-5",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "449--456",

editor = "A. Kurz and M. Lenisa and A. Tarlecki",

booktitle = "Algebra and Coalgebra in Computer Science (Third International Conference, CALCO 2009, Udine, Italy, September 7-10, 2009. Proceedings)",

address = "Germany",

}

Zantema, H 2009, A tool proving well-definedness of streams using termination tools. in A Kurz, M Lenisa & A Tarlecki (eds), Algebra and Coalgebra in Computer Science (Third International Conference, CALCO 2009, Udine, Italy, September 7-10, 2009. Proceedings). Lecture Notes in Computer Science, vol. 5728, Springer, Berlin, pp. 449-456. https://doi.org/10.1007/978-3-642-03741-2_32

A tool proving well-definedness of streams using termination tools. / Zantema, H.

Algebra and Coalgebra in Computer Science (Third International Conference, CALCO 2009, Udine, Italy, September 7-10, 2009. Proceedings). ed. / A. Kurz; M. Lenisa; A. Tarlecki. Berlin : Springer, 2009. p. 449-456 (Lecture Notes in Computer Science; Vol. 5728).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - A tool proving well-definedness of streams using termination tools

AU - Zantema, H.

PY - 2009

Y1 - 2009

N2 - A stream specification is a set of equations intended to define a stream, that is, an infinite sequence over a given data type. In [5] a transformation from such a stream specification to a TRS is defined in such a way that termination of the resulting TRS implies that the stream specification admits a unique solution. In this tool description we present how proving such well-definedness of several interesting boolean stream specifications can be done fully automatically using present powerful tools for proving TRS termination.

AB - A stream specification is a set of equations intended to define a stream, that is, an infinite sequence over a given data type. In [5] a transformation from such a stream specification to a TRS is defined in such a way that termination of the resulting TRS implies that the stream specification admits a unique solution. In this tool description we present how proving such well-definedness of several interesting boolean stream specifications can be done fully automatically using present powerful tools for proving TRS termination.

U2 - 10.1007/978-3-642-03741-2_32

DO - 10.1007/978-3-642-03741-2_32

M3 - Conference contribution

SN - 978-3-642-03740-5

T3 - Lecture Notes in Computer Science

SP - 449

EP - 456

BT - Algebra and Coalgebra in Computer Science (Third International Conference, CALCO 2009, Udine, Italy, September 7-10, 2009. Proceedings)

A2 - Kurz, A.

A2 - Lenisa, M.

A2 - Tarlecki, A.

PB - Springer

CY - Berlin

ER -

Zantema H. A tool proving well-definedness of streams using termination tools. In Kurz A, Lenisa M, Tarlecki A, editors, Algebra and Coalgebra in Computer Science (Third International Conference, CALCO 2009, Udine, Italy, September 7-10, 2009. Proceedings). Berlin: Springer. 2009. p. 449-456. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-642-03741-2_32