Software and hardware systems become more and more complex and thereby more difficult to produce with given requirements of safety and reliability. At the same time, we become as individuals, as organisations and companies and as society more and more depending on them. By giving support for modelling and verification, interactive theorem proving will give important support in the production of correct, safe, and reliable systems. The course gives an overview of different technologies for interactive theorem proving and gives an introduction to such a tool in sufficient depth, so that the students should be able to carry out a smaller modelling and verification assignment on their own. The students will learn to model complex systems formally, to verify the models against their real correspondences, as well as to use an interactive theorem prover to different forms of model analyses.
FDD3461 Interactive Theorem Proving 4.5 credits
Content and learning outcomes
Course contents
Intended learning outcomes
At the end of the course, the student should be able to
- Account for different technologies for interactive theorem proving
- Assess which types of problems interactive theorem proving is suited to solve
- Master an interactive theorem prover in detail and account for its function and limitations
- Use the theorem prover correctly on a smaller project
- Without effort use related tools
- Develop own formal models and account for limitations and applicability as well as express and formally prove important model features in the theorem prover
- Be able to design and carry out basic conformity testing
Literature and preparations
Specific prerequisites
- Functional programming
- Propositional and first order logic
Recommended prerequisites
Equipment
Literature
Examination and completion
If the course is discontinued, students may request to be examined during the following two academic years.
Grading scale
Examination
- EXA1 - Examination, 4.5 credits, grading scale: P, F
Based on recommendation from KTH’s coordinator for disabilities, the examiner will decide how to adapt an examination for students with documented disability.
The examiner may apply another examination format when re-examining individual students.
Project work and activity in the course
Opportunity to complete the requirements via supplementary examination
Opportunity to raise an approved grade via renewed examination
Examiner
Ethical approach
- All members of a group are responsible for the group's work.
- In any assessment, every student shall honestly disclose any help received and sources used.
- In an oral assessment, every student shall be able to present and answer questions about the entire assignment and solution.