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

General Information

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.

Course Material

Content Material
0. Organisation and overview slides_00.pdf and overview
1. Introduction slides_01.pdf
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

http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle/doc/tutorial.pdf

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

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.

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.

Goals of the exercises.

Sheets

No. PDF Date Prepare Remarks
1 Sheet1.pdf 12.04.10 16.04.10 German version: Blatt1.pdf
2 Sheet2.pdf 19.04.10 23.04.10
3 Sheet3.pdf 26.04.10 30.04.10
4 Sheet4.pdf 03.05.10 07.05.10 (Update: Modified Exercise 2a to be more clear.)
5 Sheet5.pdf 10.05.10 21.05.10
6 Sheet6.pdf 31.05.10 04.06.10
7 Sheet7.pdf 09.06.10
8 Sheet8.pdf 23.06.10
9 Sheet9.pdf 25.06.10
10 Sheet10.pdf 07.07.10

The remaining hardcopies of all sheets are available on the blue shelf in our working group (building 34).

Exams

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.

Contact

Dipl.-Inf. Patrick Michel