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

Timetable

Tuesday, 15:30 - 17:00 Location: 34-420
Thursday, 15:30 - 17:00 Location: 34-420
Start: 08.04.2008

Course Material

Course content and slides by courtesy of Dr. Jens Brandt.

Content	Slides/Text
Introductory Slides (Einführungsfolien)	slides_00.pdf
Introduction to ML 1	slides_01.pdf
Introduction to ML 2	slides_02.pdf
Theorem Proving Fundamentals	slides_03.pdf
Implementing a Simple Theorem Prover	slides_04.pdf
Higher-Order Logic	slides_05.pdf
Verification with Isabelle/HOL	see http://isabelle.in.tum.de/coursematerial/PSV2006/
Case study “Algorithm verification”	see quicksort theory below
Case study “Modeling of finite system”	see elevator theory below
Embedding of PDL	see Isabelle/HOL Tutorial, Sect. 6.6
Hardware verification	slides_11.pdf
Introduction to programming language semantics	slide files 1-3 at http://sct.ethz.ch/teaching/ss2004/sps/lecture.html
Semantics and Hoare logics	Printout of paper “Abstract Hoare Logics” by T. Nipkow
Theorem Proving beyond Deduction	slides_13.pdf

The newest version of the book “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

Exercises

Content	PDF-File	Comment
Handout 1 (Übungsblatt 1)	uebung01.pdf
Handout 2	exercises02.pdf
Handout 3	exercises03.pdf
Handout 4	exercises04.pdf
Handout 5	exercises05.pdf
Handout 6	exercises06.pdf
Handout 7	exercises07.pdf

Exercise material and solutions

Content	thy-File	Comment
Handout 1 Exercise 3 a	h1ex3a	byThimo Langbehn
Theory “Qsort” for Handout 5	Qsort-homework.thy	Don’t forget to rename either theory name or file name. Otherwise, the Isabelle/Isar system will complain about wrong theory name
Theory “Elevator”	Elevator0.thy	Don’t forget to rename either theory name or file name. Otherwise, the Isabelle/Isar system will complain about wrong theory name
Theory “ElevatorWithSketch”	ElevatorWithSketch.thy	Contains the elevator speicification with the sketched relation to the ML-checker implementation.
ML program “elevator.sml”	elevator.sml	Contains the ML-checker implementation.
Theory “Pdl.thy”	Pdl.thy	Contains the PDL theory from the Isabelle/HOL Tutorial
Theory “WhileLang.thy”	WhileLang.thy	Contains the semantics of a while language
Theory “MyHoare.thy”	MyHoare.thy	Contains a Hoare logic proof for a while program