Program Verification, BSc (Spring 2025)

Abstract

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.

Description

“Program testing can be used to show the presence of bugs, but never to show their absence!” ― Edsger W. Dijkstra (1970);"

The predominant method developers use to ensure that software behaves as intended, is testing. However, no amount of testing can guarantee the absence of errors. While errors in business applications are often tolerated, the same cannot be said for software found in medical equipment, or for software used by aerospace and automotive industries. In such safety-critical systems, errors lead to significant monetary losses, destroyed equipment, even loss of life.

In this course you learn how to write specifications of programs and prove, using state-of-the-art tools, that these programs follow their specification to the letter. You will write proofs in a similar way to how you write programs, and you will use interactive and automated proof assistants to check that all of your proofs are correct. Having a computer check your proofs in this way

• significantly reduces the possibility of developer error, thus greatly improving the reliability of your software
• enables you to update proofs of correctness in a similar iterative manner as you write programs---a sharp contrast to the error-prone task of maintaining and checking paper proofs.

You will also learn the theoretical underpinnings required to make these tools function, giving you a solid understanding of how programs and their proofs of correctness are connected.

This course is relevant for anyone with an interest in program correctness, as well as for mathematicians with an interest in ensuring that their pen-and-paper proofs are correct by having them checked by a computer.

You will predominately be working with two tools in this course -- Coq and Frama-C.

Coq
Coq is an industry-grade interactive proof assistant that allows users to:

• write and prove mathematical theorems
• write programs and specifications in an embedded functional language called Gallina, prove properties about these programs, compile them to executable code, and run the verified programs
• step through proofs one line at a time, similarly to a debugger, in order to modify and develop the proofs as you go along.

Frama-C
Frama-C is an industry-grade automated proof assistant for the C programming language, used by NASA, Airbus, Thales, EdF, Mitsubishi, and others. Frama-C allows you to

• analyze variables, effects, and dependencies in your C programs.
• write specifications for your C programs.
• prove that a C program satisfies its specification using third-party automatic or interactive theorem provers.

Automated proof assistants attempt to prove theorems automatically, similarly to how an IDE type checks your programs automatically. When they fail to do so, Frama-C lets you use more generally-applicable interactive theorem provers (like Coq)

Tying it all together
Coq is very expressive allowing you to reason about a wide variety of programs and theorems; Frama-C has support for a wide variety of interactive and automatic proof assistants giving you a lot of freedom in how you approach your verification tasks.

Formal prerequisites

Required

• Discrete Mathematics
• Introductory programming

Recommended

• Functional programming (it is perfectly fine to read both courses in parallel)
• Algorithms and data structures

Intended learning outcomes

After the course, the student should be able to:

• 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

Ordinary exam

Exam type:
D: Submission of written work with following oral, External (7-point scale)
Exam variation:
D2G: Submission for groups with following oral exam supplemented by the submission. Shared responsibility for the report.