Circ

Circ is an automated behavioral prover based on the circularity principle. The circularity principle generalizes both circular coinduction and structural induction and can be expressed in plain English as follows. Assume that each equation of interest (to be proved) e admits a frozen form fr(e) and a set of derived equations, its derivatives, Der(e). The circularity principle requires that the following rule be valid: if from the hypotheses H together with fr(e) we can deduce Der(e), then e is a consequence of H. When fr(e) freezes the equation at the top, the circularity principle becomes circular coinduction. When the equation is frozen at the bottom on a variable, then it becomes a structural induction (on that variable) derivation rule. This way, Circ supports both coinduction and induction as projections of a more general principle.

Web Interface to Circ

There are two methods available for running Circ. First, the Circ prover can be downloaded (see below) and run directly. This requires Maude, linked below, to be installed. Second, Circ can be executed using an online interface (click the "Try it online" icon above), which provides a place to enter and run existing or new proof scripts.

Documentation

• CIRC Tutorial and User Manual

Installation

• If you already have Maude installed, then go to the next step. Otherwise,

• if you work on a Linux platform, then go to Maude download page and follow the steps written there for downloading and installing Maude;
• if you work on a Windows platform, then download Maude for Windows;
• if you have Eclipse, then you also may download Maude Development Tools; this include a set of plug-ins embedding the Maude system into the Eclipse environment.

• Download CIRC 1.4: Circ.zip . The archive includes documentation, a set of examples, and the tool circ.maude.
• Copy the file circ.maude in the folder including Maude tools (e.g., full-maude.maude, model-checker.maude and so on).
• Follow the instructions from the manual in order to use the Circ tool.

Information about Circ is also available at the FMSE-UAIC site, Formal Methods in Software Engineering Group at Al. I. Cuza University, Romania.

Publications

Below are all our publications on matching logic, in reverse chronological order.

Automating Coinduction with Case Analysis 

Eugen-Ioan Goriac, Dorel Lucanu and Grigore Rosu
ICFEM'10, LNCS 6447, pp 220-236. 2010
PDF, LNCS, ICFEM'10, CIRC, BIB

Circular Coinduction with Special Contexts 

Dorel Lucanu and Grigore Rosu
ICFEM'09, LNCS 5885, pp 639-659. 2009
PDF, Slides(PDF), LNCS, ICFEM'09, BIB

Circular Coinduction: A Proof Theoretical Foundation 

Grigore Rosu and Dorel Lucanu
CALCO'09, LNCS 5728, pp 127-144. 2009
Slides (PDF), LNCS, CALCO'09, DBLP, BIB

CIRC: A Circular Coinductive Prover 

Dorel Lucanu and Grigore Rosu
CALCO'07, LNCS 4624, pp 372-378. 2007
PDF, CIRC webpage, CALCO'07, BIB

Hidden Logic 

Grigore Rosu
PhD Thesis, University of California at San Diego
PDF, Thesis@UCSD, BIB