# 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

### 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 (UAIC), 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
, LNCS 6447, pp 220-236. 2010ICFEM'10

PDF, LNCS, ICFEM'10, CIRC, BIBCircular Coinduction with Special Contexts- Dorel Lucanu and Grigore Rosu
, LNCS 5885, pp 639-659. 2009ICFEM'09

PDF, Slides(PDF), LNCS, ICFEM'09, BIBCircular Coinduction: A Proof Theoretical Foundation- Grigore Rosu and Dorel Lucanu
, LNCS 5728, pp 127-144. 2009CALCO'09

Slides (PDF), LNCS, CALCO'09, DBLP, BIBCIRC: A Circular Coinductive Prover- Dorel Lucanu and Grigore Rosu
, LNCS 4624, pp 372-378. 2007CALCO'07

PDF, CIRC webpage, CALCO'07, BIBHidden Logic- Grigore Rosu
, University of California at San DiegoPhD Thesis

PDF, Thesis@UCSD, BIB