Kies de Nederlandse taal
Course module: 202100115
Program Verification (Software Science)
Course info
Course module202100115
Credits (ECTS)5
Course typeCourse
Language of instructionEnglish
Contact personprof.dr. M. Huisman
Contactperson for the course
prof.dr. M. Huisman
prof.dr. M. Huisman
Academic year2022
Starting block
RemarksThis course is not on offer in 2022-2023.
Application procedure-
Registration using OSIRISNo

After successfully completing this course, the student:

  • is able to research, understand, and apply recent scientific results in software science
  • is able to answer software-related research questions on an appropriate level of abstraction

The student acquires:

  • knowledge about program semantics to reason about program properties
  • practical experience in developing tool support for static program verification
  • understanding of the issues and solutions in encoding programs and program properties in an SMT solver
  • knowledge about permission based separation logic to help reason about shared memory
  • practical experience in using a state of the art static program verification tool
  • understanding of the issues and solutions for verification of concurrent software with shared memory 

Software is everywhere, and our society is depending more and more on software working reliably and efficiently. To make it more reliable and efficient, we need to have a thorough understanding of the behavior of software systems, and how we can analyse and improve this behavior. This course gives insights in current research directions in the area of software systems, and how these new ideas can be used to improve software.
The goal of the course Software Science is to teach several topics related to active, on-going research in software engineering and formal methods. Each edition of the course consists of one topic of recent research, presented in lectures complemented with exercise or lab sessions to gain practical experiences with the material introduced during the lectures. Each topic comes with one or more individual homework/project assignments.
If one is interested in more than one topic, it is possible to follow the course a second time choosing a different topic. In this way, one can study 2 topics for 10 ECTS.

This course familiarizes students with static program verification for imperative concurrent programs, by detailing the inner workings of program verifiers. At the end of the course, a student should understand how a program verifier is built and used. We introduce the use of SMT solvers to verify software. Concepts of static software verification are introduced by discussing how to build a program that generates SMT solvers in order to verify software. We also present how to define operational and axiomatic semantics of a program, and the relation between these two semantics. We discuss how verification is further complicated when dealing with a shared heap in concurrent software.

This course is not on offer in the academic year 2022-2023.

Assumed previous knowledge
Some basic knowledge about interactive theorem proving is assumed, as is taught in the course Interactive Theorem Proving (202100126).
Participating study
Master Computer Science
Required materials
Recommended materials
Course material
Papers will be provided via Canvas
Instructional modes

Project unsupervised


Project, Exam

Kies de Nederlandse taal