Circular coinductive rewriting is a new method for proving behavioral properties, that combines behavioral rewriting with circular coinduction. This method is implemented in our n...
Abstract. CIRC is an automated circular coinductive prover implemented as an extension of Maude. The circular coinductive technique that forms the core of CIRC is discussed, togeth...
Behavioral rewriting di ers from standard rewriting in taking account of the weaker inference rules of behavioral logic, but it shares much with standard rewriting, including noti...
Coinductive proofs of behavioral equivalence often require human ingenuity, in that one is expected to provide a “good” relation extending one’s goal with additional lemmas, ...
Abstract. Coalgebra has in recent years been recognized as the framework of choice for the treatment of reactive systems at an appropriate level of generality. Proofs about the rea...