Prospectus

nl en

Programmeren & Correctheid

Course
2009-2010

Goal

The course gives an introduction to the field of verification of computer systems (hardware or software) through a series of lectures and working classes.

Description

Earliest computer programs were written largely to solve mathematical problems. In this case a program can be thought of as implicitly asserting a theorem to the effect that if certain input conditions are met then the program will solve the specific problem. Making that theorem true is not merely a matter of being an expert programmer; it can be aided by a logical analysis of what a program is supposed to do.

As programming has concentrated more on the mechanics of interacting with computer’s environment (e.g. for reactive systems and Internet applications) rather than on mathematical problems, the advantage of a logical analysis has become obvious. It is particularly difficult to foresee the effects of abnormal events on the behavior of communicating applications that may lead to inconvenient or even catastrophic situations.

A body of theory has emerged in the past two decades to make (automatic) analysis of programs a practical reality. In this course we will cover both classical and state-of-the-art core techniques in proving the correctness of computer systems.

Prerequisites

Inleiding Informatica, Logica voor Informatici

Literature

The following book will be used for the course:
Michael R. A. Huth and Mark D. Ryan Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press, 2004 (ISBN 052154310X).

Table of Contents

  1. Introduction and motivation
    a. Specification, verification and validation
    1. Modelling the dynamics of a system
      Part I : Model checking
    2. Time temporal logics
      a. Liner time temporal logic (LTL)
      b. Branching time temporal logics
      i. CTL
      ii. CTL*
      c. Using temporal logic for specification
      d. Logical equivalences
      e. Expressivity
    3. Model checking CTL
      a. The basic labelling algorithm (SAT)
      b. The correctness of SAT
      c. The fixed-point algorithm
    4. Model checking LTL
      Part II: Deductive verification
    5. A simple sequential imperative programming language
    6. Hoare logic
      a. Partial correctness
      b. Total Correctness
    7. Proof outlines
    8. The weakest (liberal) precondition calculus
    9. Reasoning about arrays

Material

Slides will be provided to the students for download.

Examination

Students will be evaluated on the basis of a written examination, possibly complemented with take-home assignments.

Practice class

Yes, a weekly practice class is a mandatory component of the course.

Website

Programmeren en Correctheid