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:

click to open video

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 19491

"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. Dijkstra2,

“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

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:

  1. program logics for writing formal correctness proofs;
  2. SMT solvers for automating reasoning about logical formulas and, thus, program proofs;
  3. 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
  4. source code verifiers for handling feature-rich programming languages.

References