CIRC: A behavioral verification tool based on circular coinduction

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

doi:10.1007/978-3-642-03741-2_30

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 proceeding › Conference 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 language	English (US)
Title of host publication	Algebra and Coalgebra in Computer Science - Third International Conference, CALCO 2009, Proceedings
Pages	433-442
Number of pages	10
DOIs	https://doi.org/10.1007/978-3-642-03741-2_30
State	Published - 2009
Event	3rd International Conference on Algebra and Coalgebra in Computer Science, CALCO 2009 - Udine, Italy Duration: Sep 7 2009 → Sep 10 2009

Publication series

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

Other

Other	3rd International Conference on Algebra and Coalgebra in Computer Science, CALCO 2009
Country	Italy
City	Udine
Period	9/7/09 → 9/10/09

ASJC Scopus subject areas

Theoretical Computer Science
Computer Science(all)

Access to Document

10.1007/978-3-642-03741-2_30

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

Cite this

Lucanu, D., Goriac, E. I., Caltais, G., & Roşu, G. (2009). CIRC: A behavioral verification tool based on circular coinduction. In Algebra and Coalgebra in Computer Science - Third International Conference, CALCO 2009, Proceedings (pp. 433-442). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5728 LNCS). https://doi.org/10.1007/978-3-642-03741-2_30

CIRC : A behavioral verification tool based on circular coinduction. / Lucanu, Dorel; Goriac, Eugen Ioan; Caltais, Georgiana; Roşu, Grigore.

Algebra and Coalgebra in Computer Science - Third International Conference, CALCO 2009, Proceedings. 2009. p. 433-442 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5728 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Lucanu, D, Goriac, EI, Caltais, G & Roşu, G 2009, CIRC: A behavioral verification tool based on circular coinduction. in Algebra and Coalgebra in Computer Science - Third International Conference, CALCO 2009, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 5728 LNCS, pp. 433-442, 3rd International Conference on Algebra and Coalgebra in Computer Science, CALCO 2009, Udine, Italy, 9/7/09. https://doi.org/10.1007/978-3-642-03741-2_30

Lucanu D, Goriac EI, Caltais G, Roşu G. CIRC: A behavioral verification tool based on circular coinduction. In Algebra and Coalgebra in Computer Science - Third International Conference, CALCO 2009, Proceedings. 2009. p. 433-442. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-642-03741-2_30

Lucanu, Dorel ; Goriac, Eugen Ioan ; Caltais, Georgiana ; Roşu, Grigore. / CIRC : A behavioral verification tool based on circular coinduction. Algebra and Coalgebra in Computer Science - Third International Conference, CALCO 2009, Proceedings. 2009. pp. 433-442 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{ba4320df51204aa5800e07553bfd2be3,

title = "CIRC: A behavioral verification tool based on circular coinduction",

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.",

author = "Dorel Lucanu and Goriac, {Eugen Ioan} and Georgiana Caltais and Grigore Ro{\c s}u",

note = "Copyright: Copyright 2009 Elsevier B.V., All rights reserved.; 3rd International Conference on Algebra and Coalgebra in Computer Science, CALCO 2009 ; Conference date: 07-09-2009 Through 10-09-2009",

year = "2009",

doi = "10.1007/978-3-642-03741-2_30",

language = "English (US)",

isbn = "3642037402",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

pages = "433--442",

booktitle = "Algebra and Coalgebra in Computer Science - Third International Conference, CALCO 2009, Proceedings",

}

TY - GEN

T1 - CIRC

T2 - 3rd International Conference on Algebra and Coalgebra in Computer Science, CALCO 2009

AU - Lucanu, Dorel

AU - Goriac, Eugen Ioan

AU - Caltais, Georgiana

AU - Roşu, Grigore

PY - 2009

Y1 - 2009

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=70350359130&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=70350359130&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-03741-2_30

DO - 10.1007/978-3-642-03741-2_30

M3 - Conference contribution

AN - SCOPUS:70350359130

SN - 3642037402

SN - 9783642037405

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 433

EP - 442

BT - Algebra and Coalgebra in Computer Science - Third International Conference, CALCO 2009, Proceedings

Y2 - 7 September 2009 through 10 September 2009

ER -