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. PDF 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.

Contact

Dipl.-Inf. Patrick Michel