Computer Laboratory

Course pages 2012–13

Interactive Formal Verification

Detailed Syllabus


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.

Note: David Damerell has solved the display issues connected with Emacs on the ACS workstations. You need to create the file .emacs on your home directory, containing the following line:

(custom-set-faces '(unicode-tokens-symbol-font-face ((t nil))))

If you have such a file already, then just insert the line, but note that you may have only one custom-set-faces command in your .emacs file!