Formal Reasoning about Software
Welcome to the official course website for CS4510 at the TU Delft!
This website contains information for the 2025/26 version of the course!
About the Course
This course is about the formal verification of software. The purpose of formal verification is to ensure the correctness of software according to a formal specification, that is, to ensure that the software has the properties stipulated by its specification. There are different methods for formal verification, e.g., model checking, but we focus on deductive verification.
We study how to verify both functional and imperative programs; in particular, we learn how to specify desired properties of such programs. We only consider functional properties, leaving out non-functional properties such as security, resource use, usability, and others.
Proving that a program has a given property can be tedious, and can, for instance, involve many case distinctions. This makes it desirable to have a computer check the correctness of our proofs. For this reason, we work with the proof assistant Coq/Rocq: we write our specifications and proofs in Coq, in a formal language. Coq checks the correctness of our proofs and notifies us of any mistakes we make.
Part of the course consists of a project, during which you write a piece of software and give and prove its specification. Substantial pieces of software are easier to verify when they are written in a functional language. Hence, in the project, we focus on the verification of a functional program. However, we also verify an imperative program as part of the project.
In industrial practice, proofs of specifications of imperative programs are often automated; see, for instance, the BSc theses in the Links section below. We will not focus on automation, but will instead understand the logical underpinning for reasoning about imperative programs: Hoare Logic.
Course Setup
Every week, we will have lectures and problem sessions.
In the lectures, we will follow the learning material very closely. In this way, you can easily catch up on any missed lectures, for instance in case of sickness.
During problem sessions, we will work on related exercises. There, you can ask the instructors and TAs for help.
You can view the material for each week in the Work Plan. Each work plan contains a list of exercises which you are expected to be able to solve. We encourage you to collaborate and pair-programme with your peers when working on these exercises. Instructors will be present during the problem sessions to help you if you get stuck.
Learning Material
We use material from the Software Foundations series of books. We will be using the local versions of these books to make sure that everyone works on the same exercises.
You can download them here:
Each chapter of these books has:
- a rendered HTML version (
<name>.html), which you can use for reading - and a raw Coq version (
<name>.v), in which you will complete the exercises.
We recommend opening the books in VS Code and using the VsCoq extension (see the installation instructions for more details) when completing the exercises.
You are welcome to work through all the exercises in the books, even if they are not highlighted within the work plan for that week. While TAs might not be able to help you with all of them, you can always ask your peers for help during the problem sessions as well as online over Mattermost (see the Contact & Help page).
Roadmap
We are going to learn about the following topics, using some of the chapters of the aforementioned books.
- Functional Programming (chapters “Basics”, “Lists”, “Poly”, “Maps”)
- Specification of Functional Programs and Proving of Specifications (chapters “Induction”, “Tactics”, “Logic”, “IndProp”, “Rel”)
- Implementation of an Imperative Programming Language (chapters “Maps”, “Imp”)
- Specifiation of Imperative Programs and Proving of Specifications (chapters “Hoare”, “Hoare2”)
Evaluation
The final grade is determined by an individual programming project in Coq. To pass, your mark must be 5.8 or higher.