Proving coinductive properties with {CIRC}

Behavioral abstraction in algebraic specification appears undervarious names in the literature such as hidden algebra (Goguen et al.),observational logic (Hennicker, Bidoit), swinging types (Padawitz),coherent hidden algebra (Diaconescu, Futatsugi), hidden logic (Rosu), andso on.  Most of these approaches appeared as a need to extendalgebraic specifications to ease the process of specifying andverifying designs of systems and also for various other reasons, suchas, to naturally handle infinite types, to give semantics to the objectparadigm, to specify finitely otherwise infinitely axiomatizableabstract data types, etc.  The main characteristic of these approachesis that sorts are split into visible (or observational)for data and hidden for states, and the equality is behavioral,in the sense that two states are behaviorally equivalent if andonly if they appear to be the same under any visible experiment. 
Coalgebraic bisimulation and context induction are sound prooftechniques for behavioral equivalence.  Unfortunately, both need humanintervention: coinduction to pick a “good” bisimulation relation,and context induction to invent and prove lemmas.Circular coinduction is an automatic proof technique for behavioral equivalence.
CIRC is an automated circular coinductive prover implemented as anextension of Maude (maude.cs.uiuc.edu).  In this talk we present the circular coinductive technique that forms the core of CIRC, together with a high-levelimplementation using metalevel capabilities of rewriting logic.To reflect the strength of CIRC in automatically proving behavioralproperties, a set of case studies including extended regular expressions, context-free processes, coinductive calculus of streams, is presented. CIRC also provides limited support for automated inductive proving, which can be used in combination with coinduction.

Sidebar