Program Verification

January 31st - June 30th, 2025

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

Lecturer(s)
Jesper Bengtson, Willard Rafnsson

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

Dates of the course
January 2025 - June 2025

Time
12-14 (lectures) 14-16 (exercises)

Room
2F14

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 two industry-grade tools for program verification in this course -- Coq and Frama-C.

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 Coq and/or Frama-C. 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 Coq and Frama-C
Construct interactive proofs that show that programs follow their specifications
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
Relate automated and interactive proof assistants and make precise the advantages and disadvantages of both types of systems

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

The Frama-C user manual (exact parts TBD)
HYPERLINK “https://frama-c.com/download/frama-c-user-manual.pdf”

The Why3 Platform (exact parts TBD) (François Bobot et al.)
HYPERLINK "http://why3.lri.fr/doc/" http://why3.lri.fr/doc/

Programme:
This course is offered to regular students, and to PhD students. This is the second 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. It was given as a PhD course in 2022.
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
Frama-C) 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. 

Project submission deadlines: The other students have mid may, with PhD students we want to be a bit more
flexible and not have a firm deadline.

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
Mini project: 30h
Main Project: 60h
Exam preparation: 10h

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