CIRC: A behavioral verification tool based on circular coinduction

Dorel Lucanu, Eugen Ioan Goriac, Georgiana Caltais, Grigore Roşu

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

Abstract

CIRC is a tool for automated inductive and coinductive theorem proving. It includes an engine based on circular coinduction, which makes CIRC particularly well-suited for proving behavioral properties of infinite data-structures. This paper presents the current status of the coinductive features of the CIRC prover, focusing on new features added over the last two years. The presentation is by examples, showing how CIRC can automatically prove behavioral properties.

Original languageEnglish (US)
Title of host publicationAlgebra and Coalgebra in Computer Science - Third International Conference, CALCO 2009, Proceedings
Pages433-442
Number of pages10
DOIs
StatePublished - 2009
Event3rd International Conference on Algebra and Coalgebra in Computer Science, CALCO 2009 - Udine, Italy
Duration: Sep 7 2009Sep 10 2009

Publication series

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

Other

Other3rd International Conference on Algebra and Coalgebra in Computer Science, CALCO 2009
Country/TerritoryItaly
CityUdine
Period9/7/099/10/09

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science

Fingerprint

Dive into the research topics of 'CIRC: A behavioral verification tool based on circular coinduction'. Together they form a unique fingerprint.

Cite this