View the course on GitHub

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 homeworks 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.

Homeworks

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

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:

Some general ideas and possible directions for custom projects:

Lecturers

The course examiner is Mads Dam.

Resources