Specification and Verification with Higher-Order Logic (SS 2010)
The lecture was held in English. The KIS entry for the course.
The lectures and exercises were on Monday, Wednesday and Friday, from 11:45 to 13:15.
The lecture started on Monday, 12.04.10. The lecture room was 48-462.
If you have any questions regarding the lecture, just contact us.
|0. Organisation and overview||slides_00.pdf and overview|
|2.a Functional programming||slides_02.pdf|
|2.b Functional specifications in Isabelle/HOL||Chapter 2 and 3 of Isabelle/HOL tutorial|
|3.a Introductory remarks on HOL||hol_introSlind.pdf|
|3.b Foundation of HOL||hol_foundations06.pdf|
|3.- Introduction to HOL (Alternative version)||slides_05.pdf|
|3.c Conservative extension in HOL||hol_conservative_extensions06.pdf|
|4.a Proof system of Isabelle/HOL||see lecture script (final version uploaded) on methods and rules, theory Lecture1.thy, and the links to theory Main below|
|4.b Proof system of Isabelle/HOL: Simplification||see slides of Sessions 2, 3.1, 3.2, and 4&5 at http://isabelle.in.tum.de/coursematerial/PSV2009-1/|
|5. Sets, functions, relations, and fixpoints||see Chapter 6 of Isabelle/HOL tutorial, theory DemoSetsFunRel.thy, and the lecture script on Knaster-Tarski|
|6. Verifying functions||see the lecture script (Fassung vom 7.6.10), and the theories on Gdc and Quicksort|
|7.a Inductively defined sets||see Chapter 6 of Isabelle/HOL tutorial and slides of Session 6.1 athttp://isabelle.in.tum.de/coursematerial/PSV2009-1/|
|7.b Specification of transitions systems||see the lecture script|
|8.a Programming language semantics in HOL||lecture slides 1-3 at http://sct.ethz.ch/teaching/ss2004/sps/lecture.html|
|8.b||see this lecture script and the theory MyWhileLang.thy|
|9.a Program verification||see this lecture script|
|9.b Program verification||based on semantics, see the theory MyWhileLang.thy|
|9.c Program verification||based on Hoare logic, see the theory MyHoare.thy|
|10 Wrap up||based on the overview
combined overview and questions
Acknowledement: We thank * Dr. Jens Brandt for the first version of the slides_xx. * Prof. Slind for the introductory remarks on HOL (hol_introSlind). * Prof. Basin, Dr. Brucker, Dr. Smaus, Prof. Wolff, and the MMISS-project for the slides on HOL (hol_foundations06, hol_conservative_extensions06). * Prof. Nipkow for the slides on Isabelle/HOL.
The newest version of the tutorial “Isabelle/HOL — A Proof Assistant for Higher-Order Logic” by Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel (originally published by Springer as LNCS volume 2283) can be found at
The following links refer to pdf-versions of the theory Main provided by Isabelle/HOL:
http://isabelle.in.tum.de/dist/library/HOL/document.pdf contains the complete theory
http://isabelle.in.tum.de/dist/Isabelle/doc/main.pdf contains a summary
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.
The exercise sheets will be handed out in the lecture and are 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.
The exercise meetings are in the SCI terminal room in 32-411.
Exercises were held on 16.04.10, 23.04.10, 30.04.10, 05.05.10, 07.05.10, 14.05.10, 21.05.10, 02.06.10, 04.06.10, 09.06.10, 11.06.10, 18.06.10, 23.06.10, 25.06.10, 28.06.10, 02.07.10, 09.07.10 and 16.07.10.
|1||Sheet1.pdf||12.04.10||16.04.10||German version: Blatt1.pdf|
|4||Sheet4.pdf||03.05.10||07.05.10||(Update: Modified Exercise 2a to be more clear.)|
The remaining hardcopies of all sheets are available on the blue shelf in our working group (building 34).
You can sign up for the exam with our secretary during her office hours or by email.
If you are interested in specific dates, please propose a day or several days which would suit you, so we can fix additional exam dates.