Formal Methods in Software Engineering

Proving Behavioral Commutativity with CIRC

Year2007
TypeConference
StatusPostproceedings
AuthorsDorel Lucanu

Links

Abstract

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.

BibTeX

@INPROCEEDINGS{dl:synasc07, author = {D. Lucanu}, title = {Proving Behavioral Commutativity with CIRC}, booktitle = {9th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing}, year = {2007}, publisher = {IEEE Computer Society}, url = {http://synasc07.info.uvt.ro [SYNASC]}, url_publisher = {http://ieeexplore.ieee.org/xpl/freeabs_all.jsp?arnumber=4438083} }