Skip to main content
Till KTH:s startsida Till KTH:s startsida

DD2452 Formal Methods 7.5 credits

Administer About course

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 will be considered.

Choose semester and course offering

Choose semester and course offering to see current information and more about the course, such as course syllabus, study period, and application information.

Application

For course offering

Autumn 2024 form24 programme students

Application code

50703

Headings with content from the Course syllabus DD2452 (Spring 2019–) are denoted with an asterisk ( )

Content and learning outcomes

Course contents

Part I. Hoare Logic and Deductive Verification

1. Code Annotation: The Java Modelling Language
2. Automated Static Assertion Checking: Weakest Preconditions
3. The Correctness-by-Construction Approach to Programming
4. Ghost State and Control-flow Abstraction
5. Model State and Data Abstraction
6. The Back-end: Automated Theorem Proving

Part II. Temporal Logic and Model Checking

7. Kripke Structures and System Modelling
8. Temporal Logic and Model Checking: LTL and CTL
9. Software Model Checking

Intended learning outcomes

The overall aim of the course is to provide a working familiarity with the main methods and tools in the formal methods area, in theory as well as in practice.

After passing the course, the students should be able to:

1. Independently select a suitable modeling approach for some given simple problem;

2. Argue informally and formally for the soundness and limitations of the chosen approach;

3. Identify, specify and verify important system properties using suitable automated or semi-automated tools;

4. Correctly interpret and evaluate the results of the analysis.

For passing the course, a student has to demonstrate the ability to apply the methods discussed in the course; for the highest grade he/she has also to be proficient in the theoretical foundations of these methods.

Literature and preparations

Specific prerequisites

A course in Discrete Mathematics, e.g. SF1630.

Recommended prerequisites

Good background in logic for computer science and discrete mathematics is required, e.g. corresponding to the courses DD1350 and SF1630.

Equipment

No information inserted

Literature

Lecture notes.

Examination and completion

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

Grading scale

A, B, C, D, E, FX, F

Examination

  • HEMA - Exercises, 2.5 credits, grading scale: P, F
  • LABA - Laboratory work, 2.5 credits, grading scale: A, B, C, D, E, FX, F
  • TENA - Examination, 2.5 credits, grading scale: A, B, C, D, E, FX, 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 final 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

Profile picture 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 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

EECS/Computer Science

Main field of study

Computer Science and Engineering

Education cycle

Second cycle

Add-on studies

No information inserted

Contact

Dilian Gurov, tel: 790 8198, e-post: dilian@kth.se

Supplementary information

In this course, the EECS code of honor applies, see:
http://www.kth.se/en/eecs/utbildning/hederskodex