• DocumentCode
    2858712
  • Title

    Proving Behavioral Commutativity with CIRC

  • Author

    Lucanu, Dorel

  • Author_Institution
    Alexandra loan Cuza Univ., Iasi
  • fYear
    2007
  • fDate
    26-29 Sept. 2007
  • Firstpage
    85
  • Lastpage
    92
  • 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;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Symbolic and Numeric Algorithms for Scientific Computing, 2007. SYNASC. International Symposium on
  • Conference_Location
    Timisoara
  • Print_ISBN
    978-0-7695-3078-8
  • Type

    conf

  • DOI
    10.1109/SYNASC.2007.70
  • Filename
    4438083
    • Link To Document
    https://search.isc.ac/dl/search/defaultta.aspx?DTC=49&DC=2858712