Formal Methods in Software Engineering (MTAT.03.274)
Formal verification is currently where functional programming was ten years ago. It is one of the hottest topics in programming language research, but it will take some time before these techniques will appear in mainstream languages. This course will, therefore, focus on key concepts underlying code correctness, allowing you to peek into the future and take home lessons to write more reliable code in any programming language.
Semantics-based techniques to reason about code will be mechanised in the proof assistant Isabelle, making these concepts concrete. Some of the lectures will thus be hands-on labs and rather informal, while others will be more conventional lectures, dry and without any sense of humour.
- Lectures / Labs:
- Tuesdays 12:15, Liivi 2-511.
- Wednesdays 16:15, Liivi 2-512.
- Textbook: Concrete Semantics with Isabelle/HOL
- Instructor: Vesal Vojdani
The course will directly follow the textbook. We first learn to write formal proofs using Isabelle, and then techniques to reason about programs are explored:
- operational semantics
- compiler correctness
- (security) type systems
- program analyses
- denotational semantics
- Hoare logic
- abstract interpretation
The last topic will be part of our programming language seminar.
Requirements & Grading
- Theorem proving is a natural continuation of functional programming. You should have some experience with functional programming (e.g., Haskell, Scala, OCaml or F#) in order to enjoy this course.
- Do not take this course if you are in an unstable relationship; theorem proving is known to be highly addictive.
- You need to attend the lectures/labs with your own laptop that has Isabelle installed.
- There will be (almost) weekly exercises. They constitute 50% of the final grade. Homework will be submitted via moodle.
- The other 50% comes from the final exam. This will be a home exam (or verification project) and a brief discussion of your solution with the instructor.