View the course on GitHub
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.
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.
The latest edition of the course material is below; there also is the course material of 2020 edition.
| Lecture | Topic | Slides |
|---|---|---|
| 1 | Introduction | |
| 2 | Basic HOL4 | |
| 3 | HOL4 proofs | |
| 4 | HOL4 definitions | |
| 5 | HOL4 embeddings | |
| 6 | HOL4 rewriting | |
| 7 | HOL4 relations | |
| 8 | HOL4 productivity | |
| 9 | Program verification | |
| 10 | CakeML | |
| 11 | ITP overview |
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.
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.
The course examiner is Mads Dam.