ETH Zuerich - Homepage
Information Security

Computer-supported Modeling and Reasoning

Master in Information Security

For more information about the Information Security Master Track visit:

An interactive course in Isabelle 2004

by A.D. Brucker, D. Basin, J.G. Smaus and B. Wolff

This comprehensive interactive course covers theory and practice of the proof-assistant Isabelle. The material has been used in previous years at the University Freiburg and the ETH Zürich in regular classes.

The course is organized into 5 larger parts covering:

  1. an introduction to logic and natural deduction,
  2. lambda-calculi and meta-logical frameworks,
  3. the meta-logical framework Isabelle and its generic proof procedures,
  4. higher-order logics(HOL): methods & library theories,
  5. introduction to HOL-applications in imperative and functional program verification, refinement and test.

The lecture material consists of about 1200 slides. The exercise block comprises 13 exercise sheets with about 54 exercises including solutions.

The material can be downloaded in several versions: for local interactive use, as global integrated document (with internal hyperlinks), and as a printable version.


Wichtiger Hinweis:
Diese Website wird in älteren Versionen von Netscape ohne graphische Elemente dargestellt. Die Funktionalität der Website ist aber trotzdem gewährleistet. Wenn Sie diese Website regelmässig benutzen, empfehlen wir Ihnen, auf Ihrem Computer einen aktuellen Browser zu installieren. Weitere Informationen finden Sie auf
folgender Seite.

Important Note:
The content in this site is accessible to any browser or Internet device, however, some graphics will display correctly only in the newer versions of Netscape. To get the most out of our site we suggest you upgrade to a newer browser.
More information

© 2011 ETH Zurich | Imprint | Disclaimer | 28 January 2011