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. An online version of the prover can be used either on the Tools page of this site or on the CIRC web page at UIUC.