Course pages 2011–12

Interactive Formal Verification

Detailed Syllabus

Slides

This lecture course introduces interactive formal proof using Isabelle. The lecture notes consist of copies of the slides, some of which have brief remarks attached. Extensive Isabelle documentation is available. In particular, you may want to read Programming and Proving in Isabelle/HOL, by Tobias Nipkow.

A valuable quick reference guide to Isabelle/HOL and Proof General has been published as a wiki page. (Please note that this page is managed outside Cambridge.)

You can run Isabelle from a Computer Laboratory Linux workstation by typing the following command:

	/usr/groups/theory/isabelle/Isabelle/bin/isabelle emacs&

You will probably want to put something in your .profile to shorten this command, either by creating an alias or by augmenting your search path.

Isabelle is easily installed on UNIX based workstations (including Apple Macs), and (with a bit of effort) on Windows using Cygwin. Full instructions are available online.

You will also need to learn how to use the text editor Emacs. Advanced skill is not necessary, merely the ability to move backward and forward in a file and to insert or delete text. Learning is not that difficult, especially because the arrow keys and mouse behave more or less as you would expect. On the Internet, you will find many helpful Emacs tutorials.