Your studies

Course syllabus for Formal methods for security

The course syllabus contains changes
See changes

Course syllabus adopted 2026-02-16 by Head of Programme (or corresponding).

Overview

  • Swedish nameFormella metoder för säkerhet
  • CodeDAT705
  • Credits7.5 Credits
  • OwnerMPALG
  • Education cycleSecond-cycle
  • Main field of studyComputer Science and Engineering
  • DepartmentCOMPUTER SCIENCE AND ENGINEERING
  • GradingTH - Pass with distinction (5), Pass with credit (4), Pass (3), Fail

Course round 1

  • Teaching language

    English

  • Application code

    02143

  • Open for exchange students

    Yes

Credit distribution

Module
Sp1
Sp2
Sp3
Sp4
Summer
Not Sp
Examination dates
0126 Project 6 c
Grading: TH		 6 c
0226 Examples class 1.5 c
Grading: UG		 1.5 c

    Examiner

    Eligibility

    Information missing

    Course specific prerequisites

    To attend the course, we recommend having completed one of the following courses:
    - Formal Methods for Software Development
    - Logic in Computer Science

    Aim

    The aim of the course is to provide students with an understanding of how formal methods can be used to specify, analyse, and verify security- and privacy-critical systems, and to give practical experience with formal specification languages and automated verification tools.

    Learning outcomes (after completion of the course the student should be able to)

    Knowledge and understanding:
    • explain the role of formal methods in specifying and verifying security-critical systems
    Competence and skills:
    • formally define and reason about key security and privacy properties using formal specification languages
    • use automated verification tools to verify compliance with security policies and detect potential vulnerabilities
    Judgement and approach:
    • critically assess the strengths and limitations of various formal techniques

    Content

    Formal methods are mathematical techniques for the specification, design, and verification of software and hardware systems. In the context of security, formal methods provide rigorous tools to model and analyze systems for potential vulnerabilities and ensure compliance with security policies. These methods enable the precise definition of security properties,  and allow for automated verification to detect flaws that may be overlooked by traditional testing. By applying formal techniques such as model checking, and theorem proving, and using formal specification languages, developers can build systems with provable security guarantees. The course consists of a series of lectures on different formalisms and verification methods that have been developed to reason about security and privacy properties. 

    Organisation

    The course consists of lectures and a project component. The lectures include compulsory quizzes. The project work involves implementing and experimenting with methods and concepts introduced in the course. Completing and presenting the project, writing a report, and participating in a code-review session are compulsory.

    Literature

    The course is based on publicly available material, such as research papers and lecture notes, which will be provided during the course.

    Examination including compulsory elements

    To pass the course, the student must pass the quizzes and make a satisfactory individual contribution to the project, including implementation, presentation, participation in an in-person code review, and submission of a written report documenting the project.

    The grading scale comprises Fail (U), 3, 4 and 5. For grade 3, the student must pass the quizzes and successfully complete the project with a functional implementation, report, presentation, and code review. Grades 4 and 5 are awarded based on the quality of the implementation, results, report, and presentation, in addition to fulfilling the requirements for grade 3.

    The course examiner may assess individual students in other ways than what is stated above if there are special reasons for doing so, for example if a student has a decision from Chalmers about disability study support.

    The course syllabus contains changes

    • Changes to course rounds:
      • 2026-05-06: Examinator Examinator changed from Andrei Sabelfeld (andrei) to Alejandro Russo (russo) by Viceprefekt
        [Course round 1]
      • 2026-04-24: Examinator Examinator Andrei Sabelfeld (andrei) added by Viceprefekt
        [Course round 1]
    Formal methods for security | Chalmers