FDD3461 Interactive Theorem Proving 4.5 credits

Interaktiv teorembevisning

Offering and execution

Course offering missing for current semester as well as for previous and coming semesters

Course information

Content and learning outcomes

Course contents *

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.

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

Course Disposition

No information inserted

Literature and preparations

Specific prerequisites *

- Functional programming

- Propositional and first order logic

Recommended prerequisites

No information inserted

Equipment

No information inserted

Literature

No information inserted

Examination and completion

If the course is discontinued, students may request to be examined during the following two academic years.

Grading scale *

P, F

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

No information inserted

Opportunity to raise an approved grade via renewed examination

No information inserted

Examiner

Mads Dam

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.

Further information

Course web

Further information about the course can be found on the Course web at the link below. Information on the Course web will later be moved to this site.

Course web FDD3461

Offered by

EECS/Theoretical Computer Science

Main field of study *

No information inserted

Education cycle *

Third cycle

Add-on studies

No information inserted

Postgraduate course

Postgraduate courses at EECS/Theoretical Computer Science