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.
Wednesday, 14:00–16:00 c.t., in building 51 room 00 006
Friday, 14:00-15:00 c.t., in building 51 room 00 006
|Exercise||Friday, 15:00–16:00, in building 51 room 00 006|
|First session||Lecture 26.04.2017
|Language of instruction||English|
You have to do all exercises.
Exercise Submission Scheme
Every Tuesday before the lecture.
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.
ExercisesExercises can be found here.
Literature & Web resources
- J. Gosling et al.: (Java SE 8 edition)
- T. Lindholm, F. Yellin: (Java SE 8 edition)
- Home page of the .G. Leavens et al.. (DRAFT), February 2007.
- B. Beckert, R. Hähnle, P. Schmitt (Eds.): , Springer-Verlag, LNCS 4334
- M. Barnet, D. Naumann: Friends Need A Bit More: Maintaining Invariants Over Shared State, February 2004
- Home page of Jahob
- V. Kuncak: Modular Data Structure Verification
- Home page of JPF
- Home page of Key-Project