Formal Methods for Java (Lecture)
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 Hoenicke1 |
| Lecture |
Tuesday, 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 23.10.12 |
| Language of instruction | English |
| Credits | 6 |
| Exams | Oral, 06.03.2013, building 052, room 00-017 |
| Course Catalog | Formale Methoden für Java2 |
News
- A new version of the file PriorityQueue.java3 with full annotations has been uploaded. This includes a workaround for a bug in the JMLTools.
- On Friday, 11.01.2013, we will have two hours of tutorial to discuss the Christmas sheet. This tutorial will be held by Jochen Hoenicke. Please send your solutions to the Christmas sheet to him (see delivery note on the sheet).
- The faculty switched from pen-and-paper evaluations to a new online evaluation system4. Please use this system in the period from January 28 until February 8 to give us some feedback on the lecture. You need the RAS login to access the system. The pages are available in German and English. Note that even though you have to log into the system your answers to the questions will be completely anonymous.
Formalia
Admission criteria
You have to do all exercises.
Exercise Submission Scheme
Every Tuesday before the lecture.
Exam
There will be oral exams. The dates of the exams will be published later.
Please register via examination office as usual.Resources
Literature & Web resources
- J. Gosling et al.: The Java Language Specification5 (third edition)
- T. Lindholm, F. Yellin: The Java Virtual Machine Specification6 (second edition)
- Home page of the JML Project7.G. Leavens et al.. JML Reference Manual8 (DRAFT), February 2007.
- B. Beckert, R. Hähnle, P. Schmitt (Eds.): Verification of Object-Oriented Software: The KeY Approach9, Springer-Verlag, LNCS 4334
- M. Barnet, D. Naumann: Friends Need A Bit More: Maintaining Invariants Over Shared State10, February 2004
- Home page of Jahob11
- V. Kuncak: Modular Data Structure Verification12
- Home page of JPF13
- Home page of Key-Project14, Release Candidate Key-1.6515
Slides and Additional Material
- Lecture 116 (23.10.2012)
- Lecture 220 (26.10.2012)
- Lecture 321 (30.10.2012)
- Lecture 422 (02.11.2012)
- Lecture 523 (06.11.2012)
- Heap.java : size24, ghost25, datagroup26, complete27
- PriorityQueue.java: size28, ghost29, datagroup30, complete3
- Test.java31
- Lecture 632 (09.11.2012)
- Lecture 733 (13.11.2012)
- Lecture 834 (16.11.2012)
- Lecture 935 (20.11.2012)
- Lecture 1039 (23.11.2012)
- jpf-aprop: Heap.java40, PriorityQueue.java41, TestPF.jpf42
- jml: TestPF.jpf43
- TestPF.java44
- Lecture 1145 (27.11.2012)
- Lecture 1246 (30.11.2012)
- Lecture 1347 (04.12.2012)
- Lecture 1448 (07.12.2012)
- Lecture 1549 (11.12.2012)
- Lecture 1650 (14.12.2012)
- Lecture 1751 (18.12.2012)
- Lecture 1852 (21.12.2012)
- Lecture 1953 (08.01.2013)
- Lecture 2054 (15.01.2013)
- Lecture 2155 (18.01.2013)
- Lecture 2256 (22.01.2013)
- Lecture 2357 (25.01.2013)
- Lecture 2458 (29.01.2013)
- Lecture 2559 (01.02.2013)
- Example: GCD.java60
- Lecture 2661 (05.02.2013)
- Examples: Mul.java62, Search.java63, BubbleSort.java64
- Lecture 2765 (08.02.2013)
- Examples: Minimum.java66, SearchWithBreak.java67
- Lecture 2868 (12.02.2013)
- Example: Triangle.java69
- Lecture 2970 (15.02.2013)
Exercises
- Exercise Sheet 071 (will be discussed in first tutorial)
- Exercise Sheet 172 (submission: 30.10.2012)
- Exercise Sheet 273 (submission: 06.11.2012)
- Exercise Sheet 374 (submission: 13.11.2012)
- Additional Material: Map.java75, Key.java76, IntKey.java77
- Exercise Sheet 478 (submission: 20.11.2012)
- Exercise Sheet 579 (submisstion: 27.11.2012)
- Additional Material: UsageChecker.java80
- Exercise Sheet 681 (submission: 04.12.2012)
- Exercise Sheet 782 (submission: 11.12.2012)
- Additional Material: Heap.java83, HeapElem.java84, IntHeapElem.java85
- Exercise Sheet 886 (submission: 18.12.2012)
- Christmas Sheet87 (submission: 08.01.2013)
- Additional Material: PostCondition.java88
- Solution: ChristmasListener.java89, Christmas.jpf90
- Exercise Sheet 991 (submission: 15.01.2013)
- Patch to run z3 with Jahob: jahob/src/smtlib/smtCvcl.ml92
- Exercise Sheet 1093 (submission: 22.01.2013)
- Exercise Sheet 1194 (submission: 29.01.2013)
- Exercise Sheet 1295 (submission: 05.02.2013)
- Exercise Sheet 1396 (submission: 12.02.2013)
- Additional Material: InsertionSort.java97
