Program Verification

January 31st - June 30th, 2024

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

Lecturer(s)
Jesper Bengtson, Willard Rafnsson

Course advertisement
https://learnit.itu.dk/local/coursebase/view.php?ciid=1175

Dates of the course
2024-01-31 – 2024-06-30

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.

All lectures will have a 15-minute break. Exercise sessions allow students to take breaks as required.

Wednesday 2024-01-31: Basics/Induction
Wednesday 2024-02-07: Polymorphism and higher-order functions (weekly assignment 1)
Wednesday 2024-02-14: Logic in Coq (weekly assignment 2)
Wednesday 2024-02-21: Inductively Defined Propositions (weekly assignment 3)
Wednesday 2024-02-28: Induction Principles (weekly assignment 4)
Wednesday 2024-03-06: 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 2024-03-13: Big-step operational semantics and Hoare Logic
Wednesday 2024-03-20: Automated proof assistants
Wednesday 2024-03-27: Frama-C: Verifying imperative programs (mini-project submission)
Wednesday 2024-04-03: Spring break
Wednesday 2024-04-10: The Why3 Platform (weekly submission 6)
Wednesday 2024-04-17: Project (weekly submission 7)

Project start
Wednesday 2024-04-23: Project
Wednesday 2024-04-30: Project
Wednesday 2024-05-8: Project
Wednesday 2024-05-15: Project

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.