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.
The course is offered every year in period 1, together with the course with the same name on the advanced level.
Course structure
Course literature
Parts of the book Michael Huth, Mark Ryan: Logic in Computer Science, and various papers.
Upon passing the course, the students will be able to:
A course in logic, corresponding to the course DD1350 Logic for Computer Science.
If the course is discontinued, students may request to be examined during the following two academic years.
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.
One needs to pass the homework assignments, the laboratory assignments, and the takehome exam.
