| Year | 2007 |
|---|---|
| Type | Conference |
| Status | Proceedings |
| Authors | Dorel Lucanu, Grigore Rosu |
Links
Abstract
CIRC is an automated circular coinductive prover implemented as an extension of Maude. The circular coinductive technique that forms the core of CIRC is discussed, together with a high-level implementation using metalevel capabilities of rewriting logic.
To reflect the strength of CIRC in automatically proving behavioral properties, an example defining and proving properties about infinite streams of infinite binary trees is shown. CIRC also provides limited support for automated inductive proving, which can be used in combination with coinduction.
BibTeX
@INPROCEEDINGS{circ:calco07,
author = {D. Lucanu and G. Roc{s}u},
title = {Circ: A Circular Coinductive Prover},
booktitle = {2nd Conference on Algebra and Coalgebra in Computer Science (CALCO 2007)},
series = {Lecture Notes in Computer Science},
volume = {4624},
pages = {372--378},
year = {2007},
editor = {T. Mossakowski and et al.},
publisher = {Springer},
url_publisher = {http://www.springer.com/computer/theoretical+computer+science/book/978-3-540-73857-2},
url = {http://www.ii.uib.no/calco07/ [CALCO07]}
}