Universität Bremen  
  FB 3  
  AG BKB > Publikationen > Suche > Deutsch

Suche nach Veröffentlichungen - Detailansicht

Art der Veröffentlichung: Artikel in Konferenzband
Autor: Daniel Hausmann, Till Mossakowski, Lutz Schröder
Herausgeber: Maura Cerioli
Titel: Iterative Circular Coinduction for {CoCASL} in {Isabelle/HOL}
Buch / Sammlungs-Titel: Fundamental Approaches to Software Engineering 2005
Band: 3442
Seite(n): 341 – 356
Serie / Reihe: Lecture Notes in Computer Science
Erscheinungsjahr: 2005
Verleger: Springer, Berlin
Abstract / Kurzbeschreibung: 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
Schlagworte: circular coinduction coalgebra CoCASL Isabelle
Status: Reviewed
Letzte Aktualisierung: 22. 06. 2005

 Zurück zum Suchergebnis
Autor: Automatisch generierte Seite
Zuletzt geändert am: 23. Februar 2006   impressum