Sciweavers

CALCO
2007
Springer

CIRC : A Circular Coinductive Prover

13 years 7 months ago
CIRC : A Circular Coinductive Prover
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.
Dorel Lucanu, Grigore Rosu
Added 12 Aug 2010
Updated 12 Aug 2010
Type Conference
Year 2007
Where CALCO
Authors Dorel Lucanu, Grigore Rosu
Comments (0)