FDD3452 Formal Methods 7.5 credits

Formella metoder

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.

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 *

  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.

Course Disposition

No information inserted

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

Dilian Gurov

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 FDD3452

Offered by

EECS/Theoretical Computer Science

Main field of study *

No information inserted

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