Universität Bremen  
  FB 3  
  Group BKB > Publications > Search > Deutsch

Publications Search - Details

Publication type: Article in Proceedings
Author: Daniel Hausmann, Till Mossakowski, Lutz Schröder
Editor: Maura Cerioli
Title: Iterative Circular Coinduction for CoCASL in Isabelle/HOL
Book / Collection title: Fundamental Approaches to Software Engineering 2005
Volume: 3442
Page(s): 341 – 356
Series: Lecture Notes in Computer Science
Year published: 2005
Publisher: Springer, Berlin
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 reactive behavior of a coalgebraic system typically rely on the method of coinduction. In comparison to `traditional' coinduction, which has the disadvantage of requiring the invention of a bisimulation relation, the method of emphcircular coinduction allows a higher degree of automation. As part of an effort to provide proof support for the algebraic-coalgebraic specification language textmdtextscCoCasl, we develop a new coinductive proof strategy which iteratively constructs a bisimulation relation, thus arriving at a new variant of circular coinduction. Based on this result, we design and implement tactics for the theorem prover Isabelle which allow for both automatic and semiautomatic coinductive proofs. The flexibility of this approach is demonstrated by means of examples of (semi-)automatic proofs of consequences of textmdtextscCoCasl specifications, automatically translated into Isabelle theories by means of the Bremen heterogeneous CASL tool set Hets.
Internet: http://www.springerlink.com/openurl.asp?genre=article&issn=0302-9743&volume=3442&spage=341
PDF Version: http://www.informatik.uni-bremen.de/~till/papers/coinduction.pdf
PostScript Version: http://www.informatik.uni-bremen.de/~till/papers/coinduction.ps
Keywords: circular coinduction coalgebra CoCASL Isabelle
Status: Reviewed
Last updated: 22. 06. 2005

 Back to result list
Author: Automatically generated page
  Group BKB 
Last updated: February 23, 2006   impressum