Program Correctness

An introduction to using predicate logic for specifying and proving the correctness of imperative programs.

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.

Back to top