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%