| Year | 2009 |
|---|---|
| Type | Conference |
| Status | Proceedings |
| Authors | Dorel Lucanu, Eugen Goriac, Georgiana Caltais, Grigore Rosu |
Links
Abstract
CIRC is a tool for automated inductive and coinductive the orem proving. It includes an engine based on circular coinduction, which makes CIRC particularly well-suited for proving behavioral properties of innite 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.
BibTeX
@inproceedings{lucanu-etal-2009-calco,
author = {Dorel Lucanu and
Eugen-Ioan Goriac and
Georgiana Caltais and
Grigore Roc{s}u},
title = {CIRC : A Behavioral Verification Tool based on Circular Coinduction},
booktitle = {CALCO 2009},
year = {2009},
series = {LNCS},
volume = {5728},
pages = {433--442},
publisher = {Springer},
url_publisher = {http://www.springer.com/?SGWID=0-102-24-0-0&searchType=EASY_CDA&queryText=5728},
url = {http://calco09.dimi.uniud.it/[CALCO]}
}