Computer Laboratory

Course pages 2016–17

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.

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 UNIX .profile to shorten this command, either by defining a shell alias or by augmenting your search path.

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