Today's software systems are commonly buggy, untrustworthy and insecure. Formal methods is an area of research that uses methods with solid mathematical foundations to model, construct and verify software/hardware systems.

This course discusses three common methods for ensuring safety and security in software systems and includes three parts:
-  Model-Level verification:  that covers model checking, a technique to model and automatically verify a system at the modelling level.
-  Program Verification: that (i) discusses formalisms to specify and derive contracts for programs, and (ii) employs the programming language Dafny to develop correct programs.
-  Information Flow Control: that deals with security analysis of Java programs to ensure integrity and confidentiality.

The course will be given during the period: 2/11, 2020 – 17/1 2021
Please sign up by 25/10, 2020

For more information see the course plan: https://kursplan.lnu.se/kursplaner/syllabus-4DV701-1.pdf

If you have any questions, please contact Narges Khakpour – narges.khakpour@lnu.se