Specification and Verification with Higher-Order Logic (SS 2012)
General Information
The lecture is in English. The KIS entries for the course and exercise.
Don’t be confused by the times and rooms, the lectures and exercises will be on three time slots per week, namely Monday, Wednesday and Thursday, from 11:45 to 13:15. Monday will always be a lecture, Wednesday an exercise. Thursday can either be a lecture or an exercise.
Here is the schedule for the Thursday slot:
| Thursday | Event | |
|---|---|---|
| 19.04. | lecture | |
| 26.04. | lecture | |
| 03.05. | exercise | |
| 10.05. | lecture | |
| 17.05. | holiday | |
| 24.05. | exercise | |
| 31.05. | lecture | |
| 07.06. | holiday | |
| 14.06. | exercise | |
| 21.06. | exercise | |
| 28.06. | lecture | |
| 05.07. | exercise | |
| 12.07. | lecture | |
| 19.07. | exercise |
The lecture starts on Monday, 16.04.10. The lecture room is 48-462.
If you have any questions regarding the lecture, just contact us.
Course Material
| Content | Material | |
|---|---|---|
| 0. Preliminaries, 1. Introduction (version with minor corrections, July 14) | slides1.pdf | |
| 2. Functional programming and modeling (1. part) | slides2a.pdf | |
| 2. Functional programming and modeling (2. part) | slides2b.pdf | |
| 3. Foundation of HOL (1. part) | slides3a.pdf | |
| 3. Foundation of HOL (2. part) | slides3b.pdf | |
| 4. A proof system for HOL (1. part) | slides4a.pdf | |
| 4. A proof system for HOL (2. part) | slides4b.pdf | |
| 5. Verifying functions (1. part) | slides5a.pdf | |
| 5. Verifying functions (2. part, extended version) | slides5b_2.pdf | |
| 6. Inductive definitions and fixed points (1. part) | slides6a.pdf | |
| 6. Inductive definitions and fixed points (2. part) | slides6b.pdf | |
| 7. Programming language semantics (1. part) | slides7a.pdf | |
| 7. Programming language semantics (2. part) | slides7b.pdf | |
| 7. Programming language semantics (3. part) | slides7c.pdf | |
| 8. Program verification (1. part, corrected) | slides8a.pdf | |
| 8. Program verification (2. part) | slides8b.pdf | |
| 8. Program verification (3. part) | slides8c.pdf | |
| 8. Program verification (4. part) | slides8d.pdf | |
| Questions for Chapters 5 - 8 | slidesQ.pdf |
Exercises
The exercises to the course make up half of the weekly meetings. As with the lecture itself, participation is not mandatory, yet the content is relevant for the exams. We strongly suggest to take the exercises seriously, attend all of them and continue working on individual tasks in the terminal rooms.
The exercise sheets will be available online.
Please at least prepare all the parts of the sheet, which are marked accordingly. We will then work on the remaining parts within the next exercise meeting. Please note that the exercises can be part of the examination, i.e., you might be asked how to solve them and/or demonstrate steps of the solution.
The exercise meetings will be in the SCI terminal room in 32-411.
Wiki
We have a wiki for you to look up information and contribute actively! You don’t need an account to view the wiki or make changes.
If you have any troubles at all with the tool we use or the theory behind it, this is the place to go!
The Wiki also contains a page with Goals of the Exercises, which might prove helpful.
Sheets
| No. | Date | Prepare | Remarks | ||
|---|---|---|---|---|---|
| 1 | Sheet1.pdf | 16.04.12 | 18.04.12 | ||
| 2 | Sheet2.pdf | 18.04.12 | 25.04.12 | ||
| 3 | Sheet3.pdf | 25.04.12 | 02.05.12 | ||
| 4 | Sheet4.pdf | 02.05.12 | 09.05.12 | ||
| 5 | Sheet5.pdf | 09.05.12 | 16.05.12 | ||
| 6 | Sheet6.pdf | 23.05.12 | - | Please use your preparation time to finish the open ends of the former sheets. | |
| 7 | Sheet7.pdf | 13.06.12 | 20.06.12 | ||
| 8 | Sheet8.pdf | 20.06.12 | - | ||
| 9 | Sheet9.pdf | 02.07.12 | - | ||
| 10 | Sheet10.pdf | 06.07.12 | 11.07.12 | Pleaseprepare at least the loop invariant for the exercise! |
Materials
| Belongs to | File | Remarks | |
|---|---|---|---|
| Sheet 1 | Hilbert.thy | A template for the translation of the proofs in the Hilbert calculus. | |
| Sheet 1 | Sheet1.Proofs.pdf | The pen and paper proofs of the first sheet. (Contains spoilers! ;-)) | |
| Chap. 2 | FunctionalSpecLanguage.thy | Theory containing the examples of 2.2 | |
| Chap. 2 | SimpleTheoremProver.thy | Theory for the first prover version in 2.3 | |
| Chap. 2 | SimpleTheoremProver2.thy | Theory for the second prover version in 2.3 | |
| Chap. 4 | ExSimp.thy | Examples about simplification (4.2) | |
| Chap. 4 | ExCaseInduct.thy | Examples about induction (4.3) | |
| Chap. 4 | ExProofAutomation.thy | Examples about induction (4.4) | |
| Sheet 5 | Isabelle/HOL Documentation | Link to the page with the Isabelle/HOL tutorial, for the compiler exercise. | |
| Sheet 5 | Compiler.thy | Template for the compiler exercise. | |
| Chap. 5 | gcd.thy | Theory for the GCD case study (5.2) | |
| Chap. 5 | QuickSort.thy | Theory for the Quicksort case study (5.4) | |
| Sheet 7 | EQSort.thy | Efficient Quicksort theory with all proofs. | |
| Sheet 7 | RQSort.thy | Refined Quicksort theory, containing the model of the efficient one. You also need the original QuickSort.thy for this. | |
| Sheet 7 | MSort.thy | Mergesort theory template, containing the model, specification and main theorems. | |
| Chap. 6 | Elevator.thy | Elevator theory, including the liveness proof! | |
| Sheet 9 | While.thy | Theory file for a while-language based on IMP. | |
| Chap. 8 | HoareIMP.thy | Hoare logic for IMP | |
| Chap. 8 | HoareIMPwp.thy | Hoare logic for IMP in WP-style | |
| Chap. 8 | HoareIMParray.thy | Hoare logic for IMP plus arrays | |
| Sheet 10 | Hoare.thy | Template for the Hoare-calculus exercise. |
Exams
We have fixed the first two time frames for exams, the first is Friday, August 3, 2012, the second Wednesday, August 29, 2012.
You can sign up for these dates with our secretary during her office hours or by email. (Please be aware that our secretary is now on vacation and will be back at July 23.)
Depending on the number of students at each date, we will additionally use Thursday, August 2, 2012 and Thursday, August 30, 2012, respectively. So please keep in mind that your exam might get moved one day.
