Formal Methods for Java

Instructors & Assistants

• Dr. Jochen Hoenicke

Date & Location

Lectures

• Tuesday 11:00 a.m. (c.t.) - 01:00 p.m., SR 02-017 Geb. 52
• Thursday 11:00 a.m. (c.t.) - 01:00 p.m., SR 00-034 Geb.51
• 3 hours per week on average
  

Exercises (Discussion Groups)

• Tuesday 10:00 a.m. (c.t) 00-016 Geb. 52
  

Summary

Recently, formal methods have been successfully used to specify and verify large software system. A current example is the Verisoft project, whose goal is to create a fully verified processor, operating system and compiler. In this lecture we will investigate the exising methods for the language Java.

The language Java was chosen because it is a mature language, with a semi-formal definition of its semantics (The Java Language Specification). However, to use mathematical reasoning, we need a precise definition of the semantics. Therefore, we will sketch the definition of an operational semantics for Java. Furthermore, we will investigate different formal methods for Java. The starting point will be the language extension JML that allows Design by Contract. This allows to add pre- and postconditions to methods and invariants to classes and loops. These assertions can be checked during runtime and this is the purpose of the JML runtime assertion checker (jmlrac). On the other hand, there are static methods, e.g., ESC/Java and Jahob, that automatically provide mathematical proofs that the Java code ensures the post-condition for each possible pre-condition. If these proofs cannot be find automatically, one can also use theorem provers that assists finding a proof manually.

In this lecture, we will present the different approaches for verification of Java code. In the exercise you can investigate different tools on small practical examples.

Exercise Sheets

• Exercise sheet 1 (22.04.2008)
• Exercise sheet 2 (29.04.2008) [Operational Semantics]
• Exercise sheet 3 (06.05.2008) [skeleton,.tar.gz]
• Exercise sheet 4 (20.05.2008)
• Exercise sheet 5 (05.06.2008) [skeleton,.tar.gz]
• Exercise sheet 6 (11.06.2008)
• Exercise sheet 7 (18.06.2008)
• Exercise sheet 8 (25.06.2008)
• Exercise sheet 9 (02.07.2008)
• Exercise sheet 10 (18.07.2008) Lösung

Slides

• Lecture 1 (22.04.2008) (demo)
  
• Lecture 2 (24.04.2008)
• Lecture 3 (29.04.2008) (demo)
• Lecture 4 (06.05.2008) (demo)
• Lecture 5 (20.05.2008) (demo)
• Lecture 6 (29.05.2008) (demo)
• Lecture 7 (03.06.2008) (demo)
• Lecture 8 (05.06.2008)
• Lecture 9 (10.06.2008)
• Lecture 10 (17.06.2008) (demo)
• Lecture 11 (19.06.2008)
• Lecture 12 (24.06.2008)
• Lecture 13 (26.06.2008)
• Lecture 14 (01.07.2008) (demo)
• Lecture 15 (08.07.2008) (demo)
• Lecture 16 (10.07.2008)
• Lecture 17 (17.07.2008)

Material

• KeY Version 0.99 (2569)

Links & Literature

• J. Gosling et al.: The Java Language Specification (third edition)
• T. Lindholm, F. Yellin: The Java Virtual Machine Specification.
• Home page of the JML Project.
• G. Leavens et al.. JML Reference Manual (DRAFT), February 2007.
• B. Beckert, R. Hähnle, P. Schmitt (Eds.): Verification of Object-Oriented Software: The KeY Approach, Springer-Verlag, LNCS 4334