CIRC is an automated (co)inductive theorem prover based on circular (co)induction.
Grigore Rosu and Dorel Lucanu. Behavioral rewrite systems and behavioral productivity. In Shusaku Iida, José Meseguer, and Kazuhiro Ogata, editors, Specification, Algebra, and Software - Essays Dedicated to Kokichi Futatsugi, volume 8373 of Lecture Notes in Computer Science, pages 296--314. Springer, 2014. bib DOI
Marcello M. Bonsangue, Georgiana Caltais, Eugen-Ioan Goriac, Dorel Lucanu, Jan J. M. M. Rutten, and Alexandra Silva. Automatic equivalence proofs for non-deterministic coalgebras. Sci. Comput. Program., 78(9):1324--1345, 2013. bib DOI
Marcello M. Bonsangue, Georgiana Caltais, Eugen-Ioan Goriac, Dorel Lucanu, Jan J. M. M. Rutten, and Alexandra Silva. A decision procedure for bisimilarity of generalized regular expressions. In Jim Davies, Leila Silva, and Adenilso da Silva Simão, editors, Formal Methods: Foundations and Applications - 13th Brazilian Symposium on Formal Methods, SBMF 2010, Natal, Brazil, November 8-11, 2010, Revised Selected Papers, volume 6527 of Lecture Notes in Computer Science, pages 226--241. Springer, 2010. bib DOI
Gheorghe Grigoras, Dorel Lucanu, Georgiana Caltais, and Eugen-Ioan Goriac. Automated proving of the behavioral attributes. In Petros Kefalas, Demosthenes Stamatis, and Christos Douligeris, editors, 2009 Fourth Balkan Conference in Informatics, BCI 2009, Thessaloniki, Greece, 17-19 September 2009, pages 33--38. IEEE Computer Society, 2009. bib DOI
Grigore Rosu and Dorel Lucanu. Circular coinduction: A proof theoretical foundation. In Alexander Kurz, Marina Lenisa, and Andrzej Tarlecki, editors, Algebra and Coalgebra in Computer Science, Third International Conference, CALCO 2009, Udine, Italy, September 7-10, 2009. Proceedings, volume 5728 of Lecture Notes in Computer Science, pages 127--144. Springer, 2009. bib DOI
Dorel Lucanu, Eugen-Ioan Goriac, Georgiana Caltais, and Grigore Rosu. CIRC: A behavioral verification tool based on circular coinduction. In Alexander Kurz, Marina Lenisa, and Andrzej Tarlecki, editors, Algebra and Coalgebra in Computer Science, Third International Conference, CALCO 2009, Udine, Italy, September 7-10, 2009. Proceedings, volume 5728 of Lecture Notes in Computer Science, pages 433--442. Springer, 2009. bib DOI
Dorel Lucanu and Grigore Rosu. Circular coinduction with special contexts. In Karin K. Breitman and Ana Cavalcanti, editors, Formal Methods and Software Engineering, 11th International Conference on Formal Engineering Methods, ICFEM 2009, Rio de Janeiro, Brazil, December 9-12, 2009. Proceedings, volume 5885 of Lecture Notes in Computer Science, pages 639--659. Springer, 2009. bib DOI
Eugen-Ioan Goriac, Georgiana Caltais, and Dorel Lucanu. Simplification and generalization in CIRC. In Stephen M. Watt, Viorel Negru, Tetsuo Ida, Tudor Jebelean, Dana Petcu, and Daniela Zaharie, editors, 11th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2009, Timisoara, Romania, September 26-29, 2009, pages 85--92. IEEE Computer Society, 2009. bib DOI
Dorel Lucanu, Grigore Rosu, and Gheorghe Grigoras. Regular strategies as proof tactics for CIRC. Electron. Notes Theor. Comput. Sci., 204:83--98, 2008. bib DOI
Georgiana Caltais, Eugen-Ioan Goriac, Dorel Lucanu, and Gheorghe Grigoras. A rewrite stack machine for ROC! In Viorel Negru, Tudor Jebelean, Dana Petcu, and Daniela Zaharie, editors, SYNASC 2008, 10th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, Timisoara, Romania, 26-29 September 2008, pages 85--91. IEEE Computer Society, 2008. bib DOI