Formal Methods in Software Engineering (MTAT.03.274)
Formal verification is currently in the state 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 focus on key concepts underlying code correctness. Semantics-based techniques to reason about code will be mechanised in the proof assistant Isabelle, making these concepts concrete. Therefore, some of the lectures will 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 (firstname.lastname@example.org)
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.
- 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.