Course pages 2014–15

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.

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

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

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 jEdit. Advanced skill is not necessary, merely the ability to move backward and forward in a file and to insert or delete text.