Confer the Fall 2022 edition for the course material and more information.

General Information

Course type: MSc, 7.5 ECTS (13 weeks)
The course spans the period E1B (Fall, see DTU’s academic calendar).
Classes take place every Thursday, from 13:00 to 17:00.
Examination: Two projects (in small groups) + oral exams
Lecturer: Christoph Matheja

This course offers a hands-on introduction to the usage, construction, and theory of automated deductive program verifiers. Students should acquire the skills to apply and extend tool-supported methodologies for developing proven-correct software.

You can read the brief course description below or watch the following (somewhat longer) video in which I will motivate why you might want to learn about program verification, give a quick demo, and outline the topics covered in the course:

What this course is about?

One of the most fundamental questions in computer science is whether the programs we write are correct. In fact, the concern about correctness is as old as computers: Alan Turing already asked in 1949¹

"how can one check a routine in the sense of making sure that it is right?”

Early on, we learn that we should test our programs to increase our confidence in the correctness of our programs. However, as adequately summarized by Turing Award winner Edsgar W. Dijkstra²,

“program testing can be very effective to show the presence of bugs, but it is hopelessly inadequate for showing their absence.”

Dijkstra went on to note that

“the only effective way to raise the confidence level of a program is to give a convincing proof of its correctness.”

This course is concerned with the principles and pragmatics of deductive program verification - techniques for deriving such correctness proofs in a machine-checkable, compositional, and automated fashion. All of the highlighted aspects play an important role:

Deductive reasoning: our proofs must be obtained by drawing only sound conclusions from well-known assumptions.
Machine-checkable: our proofs must be machine-checkable to rule out human errors and allow for changes to our programs without starting proving their correctness all over (on a piece of paper) again.
Compositional: to scale to whole software projects, we must derive proofs of large programs from existing proofs of smaller programs. Moreover, changing aspects of one software component should not affect the correctness of other components that do not depend on it.
Automated: while fully automated verification is, in general, not possible (due to known undecidability results), we want to require as little interaction from programmers as possible. Ideally, programmers should only specify the desirable properties a program.

Examples of verification technology in the wild

Ada Spark is a programming language for safety-critical application domains, such as software for airplanes, that comes with a verification toolset.
The highest levels of the Automotive Safety Integrity Level (ASIL D) strongly recommend that formal verification is applied to software implementations.
Program Verification at Microsoft
Formal Verification in Amazon's Automated Reasoning Group

What will we do in the course?

The course will cover the technology stack underlying modern deductive verification tools from the bottom up by introducing a verifier for a small core language and then progressively enriching the language with advanced features such as a mutable heap, objects, and concurrency. For each language extension, it will explain the necessary reasoning principles, specification techniques, pragmatics, and tool support. In particular, the course will introduce:

program logics for writing formal correctness proofs;
SMT solvers for automating reasoning about logical formulas and, thus, program proofs;
intermediate verification languages in which we can encode verification methodologies targeting, for example, recursive procedures, loops, termination, mathematical datatypes, mutable heap, object-oriented programs, and concurrency; and
source code verifiers for handling feature-rich programming languages.

References

Alan M. Turing. On checking a large routine. Report of a Conference on High Speed Automatic Calculating Machines, pages 67–69, 1949.

Edsger W. Dijkstra: The humble programmer, CACM 1972

Preliminaries

Course participants are expected to be familiar with basics of mathematical logic and program semantics. The necessary background can, for example, be obtained in the DTU courses 02141 and 02156.

In particular, throughout the course we will

read and write formulas in first-order predicate logic,
formally reason about the satisfiability and validity of such formulas,
read and write formal definitions (of terms, formulas, expressions, etc.) using recursive (or inductive) definitions and sets of inference rules, and
prove properties of such formal definitions, particularly using structural induction.

We give a few pointers to standard textbooks for students looking for a refresher of or an introduction to the above topics. Our notation will be close to these books. All of the listed books are available online for DTU students.

First-order Predicate Logic

A thorough introduction to first-order predicate logic is found in chapters II and III of the following standard textbook:

Heinz-Dieter Ebbinghaus, Jörg Flum, Wolfgang Thomas: Mathematical logic (3. ed.). Graduate texts in mathematics, Springer 2021, available online.

The syntax of first-order predicate logic is discussed in chapter II.3. The semantics of the logic via the satisfaction relation $\models$ is covered in chapters III.1 - III.3 Satisfiability and validity of predicate logic formulas is defined in chapter III.4.

Notation

Throughout the course, we will write logical formulas using two notations: the (easier typable) notation used by verification tools and the (more concise, perhaps easier readable) notation commonly known from mathematics (as in the book referenced above).

The table below compares both notations and summarizes the semantics of formulas $F,G,H$ in first-order predicate logic for a structure $\mathfrak{A}$ and an interpretation $\mathfrak{I}$. Here, t, t1, ..., tn are terms, that is, expressions constructed from constants, variables $x$, and function applications (interpreted by the structure $\mathfrak{A}$, e.g. standard arithmetical operations). $\mathfrak{I}(t)$ denotes the valuation of term $t$ using interpretation $\mathfrak{I}$. R denotes a relational symbol (interpreted as the relation $R^{\mathfrak{A}}$ by the structure $\mathfrak{A}$) that takes some finite number n >= 0 of terms as argument. An example is the relational symbol =, which is interpreted as the equality relation between terms by every structure under consideration. For binary relations such as =, we often use infix notation t1 = t2 instead of =(t1, t2).

We also give the semantics of $F$ using the satisfaction (or model) relation $\mathfrak{I} \models F$ (read: interpretation $\mathfrak{I}$ satisfies formula $F$); details are found in the above textbook, chapter III.3. We denote by $\mathfrak{I}[x \texttt{:=} a]$ the update of interpretation $\mathfrak{I}$ in which we assign value $a$ (taken from the universe of structure $\mathfrak{A}$) to variable $x$.

Formula `F` in tool notation	Formula $F$ in mathematical notation	Read as	$\mathfrak{I} \models F$ if and only if
`true`	$\texttt{true}$	true	always
`false`	$\texttt{false}$	false	never
`R(t1, ..., tn)`	$R t_1 ... t_n$	relation `R` of `t1`, ..., `tn`	$(\mathfrak{I}(t_1), \ldots, \mathfrak{I}(t_n)) \in R^{\mathfrak{A}}$
`t1 == t2`	$t_1 = t_2$	`t1` equals `t2`	$\mathfrak{I}(t_1) = \mathfrak{I}(t_2)$
`t2 != t2`	$t_1 \neq t_2$	`t1` does not equal `t2`	$\mathfrak{I}(t_1) \neq \mathfrak{I}(t_2)$
`G && H`	$G \wedge H$	conjunction	$\mathfrak{I} \models G$ and $\mathfrak{I} \models H$
`G \\|\\| H`	$G \vee H$	disjunction	$\mathfrak{I} \models G$ or $\mathfrak{I} \models H$
`!G`	$\neg G$	negation	not $\mathfrak{I} \models G$
`G ==> H`	$F \rightarrow G$	implication	if $\mathfrak{I} \models G$ then $\mathfrak{I} \models H$
`exists x :: G`	$\exists x (G)$	existential quantifier	there is an a in the universe of $\mathfrak{A}$ such that $\mathfrak{I}[x \texttt{:=} a] \models G$
`forall x :: G`	$\forall x (G)$	universal quantifier	for all a in the universe of $\mathfrak{A}$, we have $\mathfrak{I}[x \texttt{:=} a] \models G$

Furthermore, a formula $F$ is satisfiable if there exists an interpretation $\mathfrak{I}$ such that $\mathfrak{I} \models F$. The formula is called valid if $\mathfrak{I} \models F$ holds for every interpretation $\mathfrak{I}$.

Operational Program Semantics & Structural Induction

We recommend two standard textbooks:

Hanne Riis Nielson, Flemming Nielson: Semantics with Applications: An Appetizer. Undergraduate Topics in Computer Science, Springer 2007, available online.

Chapter 1 gives an overview, including a brief introduction to structural induction. Chapter 2 discusses operational semantics in a style similar to the one used in the lecture.

Glynn Winskel: The formal semantics of programming languages - an introduction. Foundation of computing series, MIT Press 1993, available online.

Operational program semantics is covered in chapter 2. Chapters 3 and 4 give a detailed discussion of inductive definitions, inference rules, and proving properties about such definitions using various induction principles.

Tools

Throughout the course, we will use the Viper verification infrastructure and the SMT solver Z3. Installation instructions are found below. Please bring a device on which these tools are installed to each lecture.

Viper

The Viper verification infrastructure comprises a programming language (silver but also often just called Viper) and two verification backends (called silicon and carbon).

To install Viper, first make sure that a 64-bit version (e.g. OpenJDK) of Java 11+ is installed on your machine. This may not be the default installation on your machine (for example when installing through a package manager) or the default version offered as a download. Furthermore, make sure that the JAVA_HOME environment variable points to your Java installation (details).

We will use Viper through the Viper IDE, an extension to the free, open-source editor Microsoft Visual Studio Code (VS Code for short).

To install the Viper IDE proceed as follows:

Make sure to have the latest version of VS Code (64-bit) installed.
Open VS Code
Go to the extension browser (⇧+Ctrl+X or ⇧+⌘+X)
Search for Viper (see screenshot below).
Install the extension and restart VS Code.
Create an empty file test.vpr and open it with VS Code.
The Viper extension should now install all required dependencies.
If everything works, the Viper IDE should report verification successful for the file test.vpr.

Viper IDE extension

Z3

We will also use the SMT solver Z3, originally developed by Microsoft research.

Precompiled binaries for most operating systems are available here.

Alternatively, you can use the python tool pysmt to install Z3, use the docker image, or compile Z3 yourself.

To test your installation of Z3, run the command line tool create a file test.smt2 with the following content:

(declare-const p Bool)
(assert (and p (not p))) 
(check-sat)

Running z3 test.smt2 should then output unsat.

Frequently Asked Questions

Organization

Q: What are the preliminaries for the course? How should I prepare?

A: We expect all participants to be familiar with first-order predicate logic and the basics of program semantics. The necessary background can, for example, be obtained in the DTU courses 02141 and 02156.

A brief recap of the necessary theoretical background is found on the preliminaries page.

Moreover, we expect fluency in at least one functional or object-oriented programming language.

Q: What should I do before the weekly class on Thursday?

A: There will be homework, published on this webpage, which typically consists of a reading assignment and a few exercises to work on.

Q: Why does the course not cover topic X?

A: Obviously, some choices had to be made to fit the course into the usual 13 week schedule. I would be happy if you let me know why you think that topic X is particularly relevant for program verification (and what should be removed).

Q: What are the learning objectives of the course?

A student who has met the objectives of the course will be able to:

specify functional correctness properties of imperative programs;
use automated verification tools to develop formally verified software;
justify why a program meets its specification based on sound reasoning principles;
explain the technology stack involved in building automated verification tools;
compare deductive program verification to other methods aiming at increasing confidence in software correctness;
encode verification-related decision problems to SMT (satisfiability modulo theories);
identify potential bottlenecks in existing SMT encodings;
construct sound methodologies for program verification problems, automate these methodologies via encodings to SMT, and justify the involved design decisions;
achieve the above goals in a group effort while at the same time maintaining individual accountability; and
communicate solutions to problems in a clear and precise manner.

Examination

Q: How is this course graded?

A: Your grade is determined by:

The completeness and quality of group projects (size: 2-3).
- 15% Homework: preparation for projects
- 40% Project A: build a verification tool from scratch
- 60% Project B: design a new verification methodology
An individual oral exam
- Project presentation (ca. 7min, no slides needed)
- Discussion of projects and course content (ca. 20 min)

Q: Why do the percentages for the projects and homework submissions add up to 115%?

A: For the final grade, we will assume the total percentage is 100%. The additional 15% can be seen as a potential reward for actively working on the homework tasks.

Q: Are there old exams or other material from previous years that I can check out?

A: No, because this is the first time this course is running at DTU.

Reading material

Q: Is there a book on which the course is based?

A: No. All material required for the course will be made available online via this webpage. We will occasionally provide further references but reading them is optional.

Tools and technical difficulties

Q: Which programming language do we have to use in our projects?

A: That is your choice. You can, however, ask us for recommendations :)

Q: I have problems installing one of the tools used in the course.

A: If you have followed all installation instructions step by step and still encounter issues, please contact the teacher as soon as possible.

Q: While working on one of the assignments or projects, I get strange looking errors from one of the tools. What should I do?

A: First, try to reduce your code to a minimal example that fails. If the problem persists, contact the teaching staff with that minimal example and the error.

02245 - Program Verification