Automated Verification Using Circularities

The main a of the project is to extend the Maude system with a proving engine whose kernel is given by circular coinduction and circular implementation of the structural induction. We will investigate how this framework can be used for automatic verification of programs and systems specifications. The new framework will be an alternative at the actual methods based on model-checking and static analysis of the programs.

Circ is an automated prover implemented in Full Maude as a behavioral extension of Maude and is based on the circular coinduction. CIRC inherits the performance and all analysis tools of the entire Maude system. The demonstrator implements the circularity principle, which generalizes both circular coinduction and structural induction.


CIRC Tutorial and User Manual


  • If you already have Maude 2.4 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 2.4;
  • 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: 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.

An online version of the prover can be used on the CIRC web page at UIUC.