You are here: Home › Teaching › Winter Term 2011/2012 › Formal Methods for Java

Formal Methods for Java

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 existing 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 found automatically, one can also use theorem provers that assist in finding a proof manually. In this lecture, we will present the different approaches for verification of Java code. In the exercise you will investigate different tools on small practical examples.
Course type Lecture
Instructors Jochen Hoenicke
Lecture Wednesday, 16:00–18:00 c.t., in building 106 room 00 007 (MMR)
Friday, 10:00-11:00 c.t., in building 106 room 00 007 (MMR)
Exercise Friday, 11:00–12:00, in building 106 room 00 007 (MMR)
First session Lecture 26.10.11
Language of instruction English
Credits 6
Exams Oral, Time and Place 14./15.03.2012
Course Catalog Formale Methoden für Java

 

News

  •  Solutions to the exercise sheets might be handed in at the beginning of lecture on Wednesday

Formalia

Admission criteria

You have to do all exercises.

Exercise Submission Scheme

Every Wednesday before the lecture.

Exam

 There will be oral exams.  The exam will take place on 14th or 15th of March.

Please register via examination office as usual.

Resources

Literature

Slides

Exercises