Program Verification

Organizer(s) and Lecturer(s)
Jesper Bengtson (Associate Professor, course lead),
Willard Rafnsson (Assistant Professor)

Course advertisement
Course: Program Verification BSc and MSc (Spring 2025) | learnIT

Dates of the course
January 31st - June 30th, 2026

Time
12-14 (lectures) 7 (assignments) 1 (project)

Room
2A52

Course description
This is a hands-on course that teaches you how to prove that programs are correct. You will get in-depth experience with tools for this task, as well as an understanding of the theory behind them. This course thus equips you to pursue a career in writing safety-critical systems, or in pursuing higher studies in this area.

You will predominately be working with the Rocq interactive proof assistant, which is a tool used for both mechanizing proofs in mathematics and proving programs correct.

The course culminates with a one-month project. As a PhD student you are expected to find a piece of software or a theorem that ties into your thesis work to a significant degree and that you want to prove correct using Rocq. Ideally this project should lay the foundations for a publication.

Intended Learning Outcomes

• Characterise recent developments in programming languages and verification technology
• Create programs and their specifications using Rocq
• Create models of concepts relevant to your thesis work and prove properties about them
• Construct interactive proofs in Rocq
• Compare models of programs with their real-life counterparts
• Assess accuracy of models and make precise what impact any imprecisions have on any proofs made
• Apply and reflect on theories for modelling, analyzing and constructing programs, specifications, and their proofs of correctness

Reading list
Software Foundations Volume 1, Chapters Logical Foundations (Benjamin C. Pierce et al.)
HYPERLINK "https://softwarefoundations.cis.upenn.edu/lf-current/index.html" https://softwarefoundations.cis.upenn.edu/lf-current/index.html

Software Foundations Volume 3, Verified Functional Algorithms (Andrew W. Appel)
HYPERLINK "https://softwarefoundations.cis.upenn.edu/vfa-current/index.html" https://softwarefoundations.cis.upenn.edu/vfa-current/index.html

Programme:
This course is offered to regular students, and to PhD students. This is the fifth 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 all over Denmark.

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 Rocq proof assistant before, so joint lectures make sense. The level of the mathematics required depends heavily on what parts of your thesis work you want to prove properties about. 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. Their 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. 

Project submission deadlines: 
We appreciate that PhD students have a demanding schedule with deadlines other than the ones imposed by this course. We are flexible with submissions, but ideally we want the students to hand in before June.

Prerequisites
Functional Programming
Discrete Mathematics
Algorithms and Data Structures

Exam
Project connected to their PhD thesis (most likely individual unless students come from the same research group)

Credits
7.5 ECTS (pass/fail)

Most of this course is project work and weekly submissions. By increasing their difficulty considerably,
we have effectively increased the difficulty of the course as a whole, to fit the level of a PhD course.

Amount of hours the student is expected to use on the course
Preparation for lectures: 10h
Lectures: 20h
Exercise sessions: 20h
Weekly Exercises (outside exercise sessions): 54h
Main Project: 100h

How to sign up
Please write an email to Jesper Bengtson at jebe@itu.dk.