Verificare Automata Prin Circularitati (CIRC)
The main goal 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 on the CIRC web page at UIUC.
Research Activities
2010
- implemented user input error handling
- improved parsing engine by inheriting more operations from Full Maude
- bug-fixes
- improved simplification rules integration within the system
- improved checking for special contexts by using case analysis
- added enumerable sorts and guarded equations in order to facilitate case analysis
2009
- organized the Workshop on coalgebras and circular coinduction (ARCO) – Iasi
- implemented a new version of the inference engine based on circular coinduction
- implemented a proving technique used for combining induction with circular coinduction
- defined a technique used in order to automatically prove the bisimilarity of processes
- defined an algorithm that builds the automata associated to regular expressions, according to the Berry-Sethi algorithm
- defined and implemented an algorithm for specifying the coalgebras associated to polynomial functors
- implemented a technique for verification of the proof correctness when using simplification rules
- implemented a generalization algorithm used in order to facilitate the proofs with CIRC
- improved the output of the tool
- attendances and documentation:
- Dorel Lucanu, Georgiana Goriac (Caltais) and Eugen-Ioan Goriac: Centrum Wiskunde & Informatica – Netherlands, CALCO 09 – Italy
2008
- organized the Workshop on coalgebras and circular coinduction – Timisoara, as event of SYNASC 2008
- the inductive hypothesis can be applied within special contexts described in the CIRC manual
- proved coinductive properties of streams (the example /streams/ring-cnv-shf on the CIRC Onlinepage)
- implemented the possibility of proving the associativity, commutativity, idempotence and identity element goals
- implemented the language ROC! needed for the new way of specifying proving strategies
- separated the coinduction proving rules so that each of them does only what it is designed for
- refactoring of the CIRC prover
- attendances and documentation:
- Dorel Lucanu: University of Illinois at Urbana-Champaign (UIUC) and Research Institute of Symbolic Computation (RISC) – Linz
- Gheorghe Grigoras: University of Geneva and ETH Zurich
- Georgiana Goriac (Caltais) si Eugen-Ioan Goriac: Sinaia School on Formal Verification of Software Systems, Summer School Marktoberdorf 2008 – Engineering Methods and Tools for Software Safety and Security, Timisoara – SYNASC08
2007
- conceiving of a pattern-based framework for systems development in Maude, in order to reduce the time dedicated to CIRC refactoring in the future
- accomodation of research assistents with the Maude language and system through individual study and scientifical seminaries participation
- project organization