Title :
Proving Behavioral Commutativity with CIRC
Author_Institution :
Alexandra loan Cuza Univ., Iasi
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.
Keywords :
algebraic specification; formal verification; process algebra; CIRC; Maude; automated circular coinductive prover; behavioral algebraic specification; behavioral commutativity; coinductive calculus of streams; Calculus; Computer science; Humans; Jacobian matrices; Network address translation; Scientific computing; Tail;
Conference_Titel :
Symbolic and Numeric Algorithms for Scientific Computing, 2007. SYNASC. International Symposium on
Conference_Location :
Timisoara
Print_ISBN :
978-0-7695-3078-8
DOI :
10.1109/SYNASC.2007.70
