FDD3023 Interactive Theorem Proving and Program Verification, 2020

About the Course

Interactive theorem provers (ITPs) are powerful, flexible, and reliable tools for system modelling and formal verification. A growing use of ITPs is for specification and construction of practical and trustworthy large-scale software systems.

This course at KTH gives an overview of the foundations and technologies for ITPs and how they can be applied to model, specify, and formally verify software systems, including both abstract system models and executable programs.

The course focuses on using the HOL4 theorem prover. Examination is by homework and a final project based on HOL4.

Schedule and Lecture Slides

All slides are available under the CC-BY-SA license. Slides for lectures 1 to 8 are derived from the ITP Course material by Thomas Tuerk. Slides for lecture 9 to 11 use the slide templates from the ITP Course material, but their contents are not derived from there.

Lecture	Date	Time	Location	Topic	Slides
1	Wed Jan 22	10:00 CET	room 4523, floor 5, Lindstedtsvägen 3	Introduction	pdf
2	Wed Jan 29	10:00 CET	room 1537, floor 5, Lindstedtsvägen 3	Basic HOL4	pdf
3	Wed Feb 5	10:00 CET	room 4523, floor 5, Lindstedtsvägen 3	HOL4 proofs	pdf
4	Wed Feb 12	10:00 CET	room 4523, floor 5, Lindstedtsvägen 3	HOL4 definitions	pdf
5	Wed Feb 19	10:00 CET	room 4523, floor 5, Lindstedtsvägen 3	HOL4 embeddings	pdf
6	Wed Feb 26	10:00 CET	room 4523, floor 5, Lindstedtsvägen 3	HOL4 rewriting	pdf
7	Wed Mar 4	10:00 CET	room 4523, floor 5, Lindstedtsvägen 3	HOL4 relations	pdf
8	Wed Mar 11	10:00 CET	room 4523, floor 5, Lindstedtsvägen 3	HOL4 productivity	pdf
9	Wed Mar 18	10:00 CET	online via Zoom	Program verification	pdf
10	Wed Mar 25	10:00 CET	online via Zoom	CakeML	pdf
11	Wed Apr 1	10:00 CET	online via Zoom	ITP overview	pdf

For online lectures, course participants will receive invitations for each lecture via email.

homework

All homework documents are available under the CC-BY-SA license. homework 1 to 5 are derived from the ITP Course material by Thomas Tuerk.

Homework 1 (due Tue Jan 28, 23:59 CET)
Homework 2 (due Tue Feb 4, 23:59 CET)
Homework 3 (due Tue Feb 11, 23:59 CET)
Homework 4 (due Tue Feb 18, 23:59 CET)
Homework 5 (due Tue Feb 25, 23:59 CET)
Homework 6 (due Tue Mar 10, 23:59 CET)
Homework 7 (due Fri Apr 3, 23:59 CET)

Final Project

The final part of the course is an individual project based on HOL4. Read the overview and default project description, which is available under the CC-BY-SA license. The final project is derived from the ITP Course material by Thomas Tuerk.

Key dates:

Mon Apr 6: deadline for approval by lecturers of custom project
Mon June 1: deadline for booking project presentations with lecturers
Fri June 12: deadline for approval of homework and project

Some general ideas and possible directions for custom projects:

Deeply embed a programming language or logic in HOL4, specify its semantics, and prove something about it
Encode a specific algorithm in HOL4 and verify its key correctness property
State and prove some non-trivial mathematical theorem in HOL4

Lecturers

The course examiner is Mads Dam.