Universität Bremen  
  FB 3  
  Group BKB > Teaching > SS 05 > Deutsch

[VAK 03-604.06] Specification and Verification of Java Programs


Till Mossakowski
Lutz Schröder

Mon 13:00 - 15:00 MZH 4194,
Wed 15:00 - 17:00 MZH 7230

First lecture Wednesday, April 13, 2005

In modern software development, the formal verification of program correctness plays an increasingly important role. This course is concerned with the specification and verification of object-oriented programs in Java, with particular emphasis on the Java Modeling Language (JML), which serves in particular for design level specification. There are various verification tools for JML, such as the Extended Static Checker (ESC/Java), the application of which will form a central part of the course work.

  • Gary T. Leavens, Yoonsik Cheon. Design by Contract with JML. Draft tutorial.
  • Gary T. Leavens, Albert L. Baker, and Clyde Ruby. JML: A Notation for Detailed Design. In Haim Kilov, Bernhard Rumpe, and Ian Simmonds (editors), Behavioral Specifications of Businesses and Systems, chapter 12, pages 175-188. Kluwer, 1999.

Course Material

Author: Dr. Lutz Schröder
  wg bkb 
Last updated: July 5, 2005   impressum