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