Circ

From FSL
Jump to: navigation, search

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

Online-sm.JPG

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.
  • New.gif Download CIRC 1.4: 25px-Zip_icon.png Circ.zip Info_circle.png. 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
Personal tools
Namespaces

Variants
Actions
Navigation