Topics for Seminar Presentations

* Spec#
  =====
  http://research.microsoft.com/specsharp/

  A specification environment for C#
  analogous to JML for Java

  SpecExplorer
  http://research.microsoft.com/SpecExplorer/

  Resources (Starters)
  ---------
  See Spec# web site

  The Spec# programming system:  An overview
  http://research.microsoft.com/specsharp/papers/krml136.pdf

  Mike Barnett, Rob DeLine, Manuel Fähndrich, K. Rustan M. Leino, and Wolfram Schulte
  Verification of object-oriented programs with invariants.
  http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.10.4654

  Spec# Weeky
  http://channel9.msdn.com/wiki/specsharp/homepage/

* KeY-Hoare
  =========
  http://www.key-project.org
  http://www.key-project.org/download/hoare/

  An Interactive Verification Tool for the Hoare Calculus

  Resources (Starters)
  ---------
  See KeY web site

  The KeY Tool
  http://i12www.ira.uka.de/%7Ekey/doc/2005/sosym.pdf

  KeY book (available at RISC)
  http://www.key-project.org/thebook/

  (In the "Formal Methods Course", I present the "standard" KeY
  environment, the focus of this talk should be the extension
  "KeY-Hoare")

* Maude MSOS Tool
  ===============
  http://maude-msos-tool.sourceforge.net/

  Modular Structural Operational Semantics (MSOS)
  Framework for specification of programming language semantics

  Resources (Starters)
  ---------

  Glynn Winskel "The Formal Semantics of Programming Languages"
  Chapter 2 "Introduction to Operational Semantics", available at RISC

  Peter D. Mosses "Teaching Semantics of Programming Languages with Modular SOS"
  http://www.bcs.org/upload/pdf/ewic_tfm06_paper12.pdf

  Peter D. Mosses "Modular Structural Operational Semantics"
  http://www.brics.dk/RS/05/7/index.html

  Peter D. Mosses "Modular Language Descriptions"
  http://www.springerlink.com/content/pncky61d4ufxhy5l/

  Fabricio Chalub, Christiano Braga "Maude MSOS Tool"
http://www.sciencedirect.com/science?_ob=ArticleURL&_udi=B75H1-4P8SFM8-9&_user=464415&_coverDate=07%2F28%2F2007&_alid=809860016&_rdoc=21&_fmt=high&_orig=search&_cdi=13109&_sort=d&_docanchor=&view=c&_ct=160&_acct=C000022158&_version=1&_urlVersion=0&_userid=464415&md5=50df28fefe9150e1ce3c99192b3dcb2e

  Maude MSOS Tool Manual
  http://maude-msos-tool.sourceforge.net/mmt-manual.pdf

* B / Event-B
  =======================
  http://www.event-b.org/

  Formal method for system-level modelling and specification

  Starting Point:
  - Chapter in Book
    http://www.springer.com/computer/foundations/book/978-3-540-74106-0
    (available from Wolfgang Schreiner)

  Tool: ProB Animator and Model Checker
    http://www.stups.uni-duesseldorf.de/ProB/overview.php
    * ProB: An Automated Analysis Toolset for the B Method
      http://www.stups.uni-duesseldorf.de/ProB/probpublications.php?id=225

  Tool: Rodin Platform (Eclipse-based IDE for Event-B)
    http://www.event-b.org/
    * Rodin Tutorial
      http://deploy-eprints.ecs.soton.ac.uk/10/

* muCRL
  ==============================
  http://homepages.cwi.nl/~mcrl/

  Process specification language combined with abstract data types
  mucrl toolset

  Starting Points:
  - Tutorial http://homepages.cwi.nl/~mcrl/mcrl_manual.ps
  - Book http://www.springer.com/computer/foundations/book/978-3-540-73937-1
    (available from Wolfgang Schreiner)