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
- Introduction and motivation
a. Specification, verification and validation- Modelling the dynamics of a system
Part I : Model checking - 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 - Model checking CTL
a. The basic labelling algorithm (SAT)
b. The correctness of SAT
c. The fixed-point algorithm - Model checking LTL
Part II: Deductive verification - A simple sequential imperative programming language
- Hoare logic
a. Partial correctness
b. Total Correctness - Proof outlines
- The weakest (liberal) precondition calculus
- Reasoning about arrays
- Modelling the dynamics of a system
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.