Specification and Verification with Higher-Order Logic (SS 2014)

News

(18.07.2014) The next additional exercise will be on Tuesday (July 22th).

(06.07.2014) The additional exercise this week will be on Tuesday (July 8th).

(10.06.2014) Next week there will be a lecture on Monday (23.06.) and exercises on Wednesday and Thursday.

(13.06.2014) The next additional exercise will be on Tuesday, due to a conflict with an other exercise. The next dates will be: June 17, Tuesday; June 23, Monday; July 1, Tuesday; July 7, Monday July 8, Tuesday; July 15, Tuesday; July 22, Tuesday; July 21, Monday; July 29, Tuesday. Mondays 10am in 34-420 and Tuesdays 10am in 32-439 (or 32-411 if the room is occupied).

(30.05.2014) There will be no additional exercise on next Monday (02.06).

(16.05.2014) The additional exercise will now always be Mondays at 10am in 34-420.

(07.05.2014) The next additional exercise about functional programming will be on Monday, 12.05. at 10am in 34-420.

(30.04.2014) If you are interested in additional exercises about functional programming, please fill out this doodle before the lecture on Monday. Please choose times on which you are available each week.

General Information

The lecture is in English. The KIS entries for the course and exercise.

Course Material

Content Slides 1on1 Slides 4on1 Comment
1. Introduction Chap1_1on1.pdf Chap1_4on1.pdf
2. Functional programming and modeling Chap2_1auf1.pdf Chap2_4on1.pdf
3. Foundation of HOL Chap3_1auf1.pdf Chap3_4on1.pdf
4. A proof system for HOL Chap4_1auf1.pdf Chap4_4on1.pdf
5. Verifying functions Chap5_1auf1.pdf Chap5_4on1.pdf improved slides 273/274 (22.5.14)
6. Inductive definitions and fixed points Chap6_1auf1.pdf Chap6_4on1.pdf
7. Programming language semantics Chap7_1auf1.pdf Chap7_4on1.pdf two additional slides (22.6.14)
8. Program verification (part a) Chap8a_1auf1.pdf Chap8a_4on1.pdf
8. Program verification (part b) Chap8b_1auf1.pdf Chap8b_4on1.pdf updated (7.7.14)
8. Program verification (part c) Chap8c_1auf1.pdf Chap8c_4on1.pdf
8. Program verification (part d) Chap8d_1auf1.pdf Chap8d_4on1.pdf extended (22.7.14)
Questions for Chapters 5 - 8 Questions_1auf1.pdf Questions_4auf1.pdf

Materials

Belongs to File Remarks
Chap. 4 Lecture.thy Some examples for rule applications (4.1)
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)
Chap. 5 Gcd.thy Theory for the GCD case study (5.2)
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 without bounds
Chap. 8 techrep_logic.pdf Technical Report about logic for Java KE
Chap. 8 techrep_listex.pdf Verifcation of the List-class

Exercises

For the exercises we use the tool Isabelle2013-2, which is available to download for all major operation systems and already installed on the SCI terminals. Please note that most of the provided theories will not work with older or newer versions of Isabelle.

The exercises to the course make up half of the weekly meetings. As with the lecture itself, participation is not mandatory. We strongly suggest to take the exercises seriously, attend all of them and continue working on individual tasks in the terminal rooms. 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.

An exercise sheet usually includes several kinds of tasks:

  • Some tasks should be prepared before the exercise and are marked accordingly.
  • Some tasks are marked as hand-in. You should work on those tasks by yourself or in a small group. You can submit your solution to p_zeller@cs.uni-kl.de if you want to get feedback on your solution.
  • The other tasks are meant to be done during the exercise sessions. If you are not able to finish them in the exercise, you should work on them by yourself.

The exercise sheets will be available online. 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!

Sheets

No. PDF Prepare Material Remarks
1 PDF Wednesday, April 30 Sheet1_template.thy
Solution for exercise 1a)-c)
2 PDF Wednesday, May 7 SimpleTheoremProver2.thy
Sheet2_1f4_solution.thy
3 PDF Wednesday, May 21 Sheet3_Rewrite.thy
Sheet3_Primes.thy
4 PDF Wednesday, May 28 Sheet4_qsort.thy
Sheet4_exprsimp.hs
5 PDF Wednesday, June 2 Sheet5_inductive.thy
Sheet5_inductive_completeness.thy
6 PDF - Sheet6_Elevator.thy Sheet6_Elevator_solved.thy
7 PDF Wednesday, June 18 Sheet7_bigstep.thy
Sheet7_bigstep_ext.thy
8 PDF - Sheet8_smallstep.thy
9 PDF - Sheet9_hoare.thy
10 PDF - Sheet10_hoare_procedure.thy
Sheet10_hoare_choice.thy
Sheet10_hoare_termination.thy
11 PDF - Sheet11_theories.zip
12 PDF - Proof

You can submit your solution (or parts of it) to p_zeller@cs.uni-kl.de.

Additional Exercise on Functional Programming

No. Material
1 fpExercise1.thy
2 fpExercise2.thy
3 (blackboard)
4 aExercise4.thy
Additional exercises for termination proofs can be found on Sheet 7 and Sheet 8 of the SE1 course. Note that most of those functions are partial, which means that it will not be possible to prove termination for all parameters.
5 aExercise5.thy

Exams

We will have oral exams. Please write a mail to our secretary Judith Stengel to register for the exam. The mail should include your name, your student identification number, and the date on which you want to take the exam.

Contact

M. Sc. Peter Zeller