TU Delft
print this page print this page     
2017/2018 Electrical Engineering, Mathematics and Computer Science Master Computer Science
Software Verification
Responsible Instructor
Name E-mail
Dr. R.J. Krebbers    R.J.Krebbers@tudelft.nl
Contact Hours / Week x/x/x/x
Education Period
Start Education
Exam Period
Course Language
Course Contents
How can we ensure that software cannot crash and is guaranteed to be correct? In this course we tackle this question by viewing programs and programming languages as mathematical objects. That way we can use logic to prove properties about programs and thereby guarantee that software is correct. To make reasoning about actual programs and programming languages feasible, we will not be doing these proofs by hand, but instead use a tool called a proof assistant to build proofs that can be checked by a computer. The proof assistant that we will be using is called Coq. As we will show during this course, proof assistants turn doing proofs and logic into programming.

This course assumes familiarity with functional programming and elementary logic.

This course is a specialization course for programming languages and software engineering
Study Goals
After this course students will be able to:

- State and prove properties of functional programs in logic.
- Specify the semantics of an (imperative) programming language in logic.
- State and prove the correctness of program transformations.
- Use Hoare logic to prove properties of imperative programs.
- Use the Coq proof assistant to specify and prove correct a non-trivial program.
Education Method
This course consists of a weekly lecture of 2 hours and a lab session of 4 hours. During the lab sessions students will work on proving simple theorems. Towards the end of the course students will carry out research projects that apply the ideas of the course.
Literature and Study Materials
Main course material:

Software Foundations
Benjamin C. Pierce et al.
Freely available online at http://www.cis.upenn.edu/~bcpierce/sf/current/

Supplementary material:

Types and Programming Languages
Benjamin C. Pierce
MIT Press
ISBN 0-262-16209-1
The final grade consists of the following parts:

- A programming project in the Coq proof assistant.
- A written exam

Both have weight 50% and both should be 5.8 or higher. The weighted average should be 5.8 or higher. There is an oral resit for the written exam.

In order to participate in the exam, it is mandatory to submit homework each week. The homework will be graded on the scale [inadequate, fair, good, excellent], and all of the homework is required to compile and should be graded at least "fair".

The research project and homework should be done individually.