Skip to main content
Till KTH:s startsida

FDD3452 Formal Methods 7.5 credits

Formal methods are a collection of techniques and notations based on formal logic and formal semantics, applied to the modelling and analysis of software and hardware systems. Their main purpose is to provide unambiguous specifications of system requirements. Formal verification of the requirements allows to discover errors and bugs, and in particular design flaws that cannot be easily discovered using testing or simulation alone. The course gives a broad introduction to the subject, covering the principles and algorithmic methods behind the tools for software analysis and verification. In particular, deductive verification based on Hoare logic, and model checking based on Temporal logic are considered.

Information per course offering

Termin

Information for Autumn 2024 Start 26 Aug 2024 programme students

Course location

KTH Campus

Duration
26 Aug 2024 - 27 Oct 2024
Periods
P1 (7.5 hp)
Pace of study

50%

Application code

51275

Form of study

Normal Daytime

Language of instruction

English

Course memo
Course memo is not published
Number of places

Places are not limited

Target group
No information inserted
Planned modular schedule
[object Object]
Schedule
Schedule is not published
Part of programme
No information inserted

Contact

Examiner
No information inserted
Course coordinator
No information inserted
Teachers
No information inserted
Contact

Dilian Gurov (dilian@kth.se)

Course syllabus as PDF

Please note: all information from the Course syllabus is available on this page in an accessible format.

Course syllabus FDD3452 (Autumn 2019–)
Headings with content from the Course syllabus FDD3452 (Autumn 2019–) are denoted with an asterisk ( )

Content and learning outcomes

Course contents

  1. Automated Deductive Verification
  2. Automated Theorem Proving
  3. Temporal Logic
  4. Model Checking
  5. Predicate Abstraction

Course structure

  • 7 two-hour lectures
  • 7 two-hour tutorial sessions
  • 6 homework assignments, peer-reviewed at the tutorial sessions
  • 2 laboratory assignments
  • 1 final takehome exam, defended orally

Course literature

Parts of the book Michael Huth, Mark Ryan: Logic in Computer Science, and various papers.

Intended learning outcomes

Upon passing the course, the students will be able to:

  1. Model program behaviour.
  2. Formalize requirements on program behaviour.
  3. Express requirements for verification with tools.
  4. Verify requirements with tools.
  5. Explain the theory and algorithms behind the tools.

Literature and preparations

Specific prerequisites

No information inserted

Recommended prerequisites

A course in logic, corresponding to the course DD1350 Logic for Computer Science.

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 - Written exam, 7.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.

Other requirements for final grade

One needs to pass the homework assignments, the laboratory assignments, and the takehome exam.

Opportunity to complete the requirements via supplementary examination

No information inserted

Opportunity to raise an approved grade via renewed examination

No information inserted

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.

Further information

Course room in Canvas

Registered students find further information about the implementation of the course in the course room in Canvas. A link to the course room can be found under the tab Studies in the Personal menu at the start of the course.

Offered by

Main field of study

This course does not belong to any Main field of study.

Education cycle

Third cycle

Add-on studies

No information inserted

Contact

Dilian Gurov (dilian@kth.se)

Postgraduate course

Postgraduate courses at EECS/Theoretical Computer Science