Wednesday 5/11 REFRESHER EXERCISE CLASS HOARE LOGIC ONLY!

College Formele Methoden 2007

Formele methoden

The lectures are based on D. Peled, Software Reliability Methods, Springer 2001, ISBN 0-387-95106-7, handouts and lectures. To be studied:

Introduction - read.
Preliminaries - should be familiar.
Logic and Theorem Proving - 3.1-3.8 should be familiar, 3.8 - 3.11 should be studied, additionally the PVS handouts should be studied.
Modelling software systems - read.
Formal Specification - 5.1, 5.2, 5.4 should be studied, additionally the handouts from Huth and Ryan (pp. ) should be studied, especially the checking algorithm.
Automatic Verification - read 6.14, 6.15.
Deductive Software Verification - Hoare logic should be familiar, read 7.6, 7.7 for reflections on the appraoach.
Process Algebra and Equivalences - 8.1 - 8.6 should be studied, additionally the FDR handouts should be studied, especially thye checking algorithm.
Software Testing - 9.1 - 9.4, 9.11, 9.12.
Combining Formal Methods - recommended but not required for the exam.
Visualization - skip.
Conclusions - skip.

Additionally, the lectures by Van Gerwen (no slides available for company-reasons) and Huizing are to be studied. Available for copying at the secretaries office (HG 7.24 - if not open, see my post box opposite for the material) as handed out at the lectures: PVS handouts, Huth and Ryan handouts, I_Mathic paper, FDR handouts. The (still somewhat sketchy) handouts and Huizing's lecture can be found below.

Written examination; use of books, handouts etc. allowed.