Specification and Verification with HigherOrder 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 34420 and Tuesdays 10am in 32439 (or 32411 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 34420.
(07.05.2014) The next additional exercise about functional programming will be on Monday, 12.05. at 10am in 34420.
(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 WPstyle  
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 Listclass 
Exercises
For the exercises we use the tool Isabelle20132, 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 handin. You should work on those tasks by yourself or in a small group. You can submit your solution to p_zeller@cs.unikl.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 32411.
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.  Prepare  Material  Remarks  

1  Wednesday, April 30  Sheet1_template.thy Solution for exercise 1a)c) 

2  Wednesday, May 7  SimpleTheoremProver2.thy Sheet2_1f4_solution.thy 

3  Wednesday, May 21  Sheet3_Rewrite.thy Sheet3_Primes.thy 

4  Wednesday, May 28  Sheet4_qsort.thy Sheet4_exprsimp.hs 

5  Wednesday, June 2  Sheet5_inductive.thy Sheet5_inductive_completeness.thy 

6    Sheet6_Elevator.thy  Sheet6_Elevator_solved.thy  
7  Wednesday, June 18  Sheet7_bigstep.thy Sheet7_bigstep_ext.thy 

8    Sheet8_smallstep.thy  
9    Sheet9_hoare.thy  
10    Sheet10_hoare_procedure.thy Sheet10_hoare_choice.thy Sheet10_hoare_termination.thy 

11    Sheet11_theories.zip  
12    Proof 
You can submit your solution (or parts of it) to p_zeller@cs.unikl.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.