CIRC: A circular coinductive prover

Dorel Lucanu, Grigore Roşu

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish (US)
Title of host publicationAlgebra and Coalgebra in Computer Science - Second International Conference, CALCO 2007, Proceedings
PublisherSpringer-Verlag Berlin Heidelberg
Pages372-378
Number of pages7
ISBN (Print)9783540738572
DOIs
StatePublished - 2007
Event2nd International Conference on Algebra and Coalgebra in Computer Science, CALCO 2007 - Bergen, Norway
Duration: Aug 20 2007Aug 24 2007

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume4624 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other2nd International Conference on Algebra and Coalgebra in Computer Science, CALCO 2007
CountryNorway
CityBergen
Period8/20/078/24/07

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'CIRC: A circular coinductive prover'. Together they form a unique fingerprint.

Cite this