Program Correctness

Authors

Abstract

In this course, we address one of the fundamental questions of computer science: how do we specify what a program written in an imperative programming language (such as Java) should do, and how can we use logic to prove that our program is correct, viz. that it actually does what it is supposed to do. In this course, we learn how to use predicate logic for the specification and verification of the correctness of imperative programs.

Learning outcomes. At the end of this course, the student has:

learned to apply predicate logic in the formulation of arithmetical relations between (program) variables
basic knowledge of the proof theory of correctness of simple imperative programs
basic knowledge of the proof theory of correctness of recursive imperative programs
learned to apply proof theory in the description of correct formal proofs
learned to give concrete counterexamples in the case of incorrect programs
basic knowledge of meta-theoretical aspects such as soundness, completeness, and decidability
experience with computer-assisted theorem proving

Topics

Placeholder text for the list of topics covered in this course.

Schedule

Placeholder text for the weekly schedule.

Materials

Placeholder text for lecture notes, slides, and reading list.

Assessment

Placeholder text for the assessment scheme.

History

This course was previously offered at Leiden University. See the course entry in the Leiden University study guide archive.