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

Exam

Oral exams will take place on August 6 - 8 and on September 5. You can sign up for the exam with our secretary during her office hours or by email.

Contact

%MAREK_LINK%