Course syllabus for Formal methods in software development

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

Overview

  • Swedish nameFormella metoder i mjukvaruutveckling
  • CodeDAT650
  • Credits7.5 Credits
  • OwnerMPALG
  • Education cycleSecond-cycle
  • Main field of studyComputer Science and Engineering, Software 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 02137
  • Block schedule
  • Open for exchange studentsYes

Credit distribution

0124 Laboratory 2.5 c
Grading: UG		2.5 c0 c0 c0 c0 c0 c
0224 Examination 5 c
Grading: TH		5 c0 c0 c0 c0 c0 c
  • 31 Okt 2024 pm J
  • 19 Aug 2025 pm J

In programmes

Examiner

Information missingGo to coursepage (Opens in new tab)

Eligibility

General entry requirements for Master's level (second cycle)
Applicants enrolled in a programme at Chalmers where the course is included in the study programme are exempted from fulfilling the requirements above.

Specific entry requirements

English 6 (or by other approved means with the equivalent proficiency level)
Applicants enrolled in a programme at Chalmers where the course is included in the study programme are exempted from fulfilling the requirements above.

Course specific prerequisites

The course builds on skills in first-order logic and temporal logic, acquired in DAT060 Logic in Computer Science or in SSY165 Discrete Event Systems. Skills in object-oriented programing (like Java) are also assumed.

Aim

The aim of this course is to teach knowledge and skills in, and judgement about, two important styles of formal methods for reasoning about software: model checking and deductive verification. Each style will be introduced in three ways: conceptual, theoretical, and practical, using a particular tool. The course builds on skills in first-order logic and temporal logic, and shows how these formalisms can be applied, and extended, for the verification of software.

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

On successful completion of the course the student will be able to:

Knowledge and understanding
  • explain the potential and limitations of using logic based verification methods for assessing and improving software correctness
  • identify what can and what cannot be expressed by certain specification/modeling formalisms
  • identify what can and cannot be analyzed with certain logics and proof methods,
Skills and abilities
  • express safety and liveness properties of (concurrent) programs in a formal way
  • describe the basics of verifying safety and liveness properties via model checking
  • successfully employ tools which prove or disprove temporal properties
  • write formal specifications of object-oriented system units, using the concepts of method contracts and class invariants
  • describe how the connection between programs and formal specifications can berepresented in a program logic
  • verify functional properties of simple programs with a verification tool
Judgement and approach
  • judge and communicate the significance of correctness for software development
  • employ abstraction, modelling, and rigorous reasoning when approaching the development of correctly functioning software

Content

This course covers topics in model checking and deductive verification.


On the model checking side, we cover the following topics:
  • a specification language for concurrent processes
  • verifying assertions
  • synchronization
  • verifying safety and liveness properties in temporal logic

On the deductive verification side, we cover the following topics:

  • program logics, including Hoare logic and separation logic
  • reasoning about loops using invariants
  • verification of small programs using tools for program verification
  • techniques used when tackling verification of larger or more complex programs

Organisation

There are usually two lectures each week, and one exercise class per week. The students perform practical case studies using the tools in the laboratory assignments.

Literature

See separate literature list.

Examination including compulsory elements

There are lab hand-ins that are normally done in groups of two. At the end of the course, there is a written exam. The lab-hand ins and the written exam can be passed independently. To pass the whole course, it is necessary to pass both written exam and the labs. In case of pass, the grade is determined by the result in the written exam.

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 on educational support due to disability.