TY - GEN
T1 - CIRC
T2 - 2nd International Conference on Algebra and Coalgebra in Computer Science, CALCO 2007
AU - Lucanu, Dorel
AU - Roşu, Grigore
N1 - Copyright:
Copyright 2020 Elsevier B.V., All rights reserved.
PY - 2007
Y1 - 2007
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=38049087152&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=38049087152&partnerID=8YFLogxK
U2 - 10.1007/978-3-540-73859-6_25
DO - 10.1007/978-3-540-73859-6_25
M3 - Conference contribution
AN - SCOPUS:38049087152
SN - 9783540738572
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 372
EP - 378
BT - Algebra and Coalgebra in Computer Science - Second International Conference, CALCO 2007, Proceedings
PB - Springer
Y2 - 20 August 2007 through 24 August 2007
ER -