Programme: This course is offered to regular students, and to PhD students. This is the first time this course has its own elective but I have taught it for the past ten years as part of other courses, and frequently for PhD students from ITU, DTU and KU.
Regardless of student level this is a difficult course with a heavy focus on logics and mathematics. It is not likely that students have come across large parts of the curriculum or the tools that we use (Coq and Spark ADA) before, so joint lectures make sense. The level of the mathematics required depends heavily on what type of software it is you want to prove correct. The weekly exercises in the reading material are substantial and can be trimmed to fit the level of the student.
The level of the course largely depends on the application of the curriculum and the tools we use. PhD students will leverage their previous degrees to formalise more advanced mathematics, and prove correctness of more complicated programs, than the other students. For PhD students this means in practice that:
- They are not allowed to work in groups for the weekly assignment
- The weekly assignments are larger and cover a wider curriculum than for the other students in order to prepare them for more advanced projects.
- The mini-project requires that they verify a much more complicated data structure than the other students (red-black threes as opposed to binary search trees and/or insertion sort)
- Their final larger project must be relevant to their research. This means that, unless the students happen to work in the same research group, the projects must be individual. Regardless, the scope of the project scales with the number of participants.
All lectures will have a 15-minute break. Exercise sessions allow students to take breaks as required.
Wednesday 2022-02-02: Basics/Induction
Wednesday 2022-02-09: Polymorphism and higher-order functions (weekly assignment 1)
Wednesday 2022-02-16: Logic in Coq (weekly assignment 2)
Wednesday 2022-02-23: Inductively Defined Propositions (weekly assignment 3)
Wednesday 2022-03-02: Induction Principles (weekly assignment 4)
Wednesday 2022-03-09: Curry-Howard and program extraction (weekly assignment 5)
mini-project start, (Software Foundations Volume 3)
- Regular students: Insertion sort and/or binary search trees
- PhD students: red-black trees
Wednesday 2022-03-16: Big-step operational semantics and Hoare Logic
Wednesday 2022-03-23: Automated proof assistants
Wednesday 2022-03-30: SPARK Ada: Verifying imperative programs (mini-project submission)
Wednesday 2022-04-06: The Why3 Platform (weekly submission 6)
Wednesday 2022-04-13: Spring break
Wednesday 2022-04-20: Project (weekly submission 7)
Project start
Wednesday 2022-04-27: Project
Wednesday 2022-05-04: Project
Wednesday 2022-05-11: Project
Wednesday 2022-05-18: Project
Wednesday 2022-05-25: Project submission LearnIT
Thursday 2022-06-16: Oral Exam
Friday 2022-06-17: Oral Exam