Proving Behavioral Commutativity with CIRC

CIRC is an automated circular coinductive prover implemented as an extension of Maude. In this paper we extend CIRC with the capability to prove behavioral commutativity and we show that the method is sound. The strength of the extended version of CIRC is illustrated on the example of coinductive calculus of streams.

Sidebar