You are here: Home › Teaching › Summer Term 2017 › Formal Methods for Java (Lecture)

Formal Methods for Java (Lecture)

In this lecture we will investigate the existing methods for formally verifying object oriented languages like 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 (rac). On the other hand, there are static methods, e.g., extended static checking (esc) 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, Alexander Nutz
Lecture Wednesday, 14:00–16:00 c.t., in building 51 room 00 006
Monday, 14:00-15:00 c.t., in building 51 room 03 026 (updated)
Exercise Monday, 15:00–16:00, in building 51 room 03 026 (updated)
First session Lecture 26.04.2017
Language of instruction English
Credits 6
Exams Wedneesday, September 27th, 2017
Course Catalog here

 

News

  • (28 June): Exercise sheet 9 will come out one day late, i.e., tomorrow. The deadline for handing in solutions will thus be one day later than usual, too.
  • (11 May): Exercise sheet 3 will come out one day late (i.e. today). The deadline for handing in solutions will thus be one day later than usual, too. EDIT: It is out now (~17:30).
  • (3 May, 16:20): slightly updated the exercise sheet -- please download again if you downloaded it before.
  • (3 May): We changed the time slot for the one-hour lecture and the tutorial to Monday 14-16 c.t.. Note that the room has changed, too. It now is 51-03-026. The changes apply in this week already, so this Friday there will be no lecture/tutorial, but on the following Monday there will be.
  • (28 April): The time slot on Friday seems to be non-ideal. Please enter your preferences in this doodle link, so we can hopefully find a better slot.

Formalia

Admission criteria

You have to do all exercises.

Exercise Submission Scheme

Every Tuesday before the lecture.

Exam

There will be oral or written exams, probably oral. The dates of the exams will be published later.

Please register via examination office as usual.

Resources

Slides

  • Lecture 1: Introduction to Java + JML slides, demos
  • Lecture 2: Operational Semantics (1) slides
  • Lecture 3: Operational Semantics (2) slides
  • Lecture 4: Semantics of Exceptions slides
  • Lecture 5: Semantics of JML slides
  • Lecture 6: Introduction to JML slides
  • Lecture 7-8: Abstract Data Types slides
  • Lecture 9: Introduction to ESC slides
  • Lecture 10: How ESC works slides
  • Lecture 11: Key Basics (1): Sequence Calculus slides
  • Lecture 12: Soundness of Sequence Calculus slides
  • Lecture 13: Dynamic Logic slides
  • Lecture 14: Key Examples: demos
  • Lecture 15: Object Invariants: slides
  • Lecture 16: Invariants and Friendship: slides
  • Lecture 17-18: Framing in Key: slides
  • Lecture 19: Model Checking and JVM: slides
  • Lecture 20: Introduction to Java Pathfinder: slides
  • Lecture 21: Properties and Listener in JPF: slides
  • Lecture 22: JPF and Design by Contract: slides, demos
  • Lecture 23: Software Model Checking: slides
  • Lecture 25: Hints for the Exam: slides

Exercises

Exercises can be found here.

Literature & Web resources