Department of Computer Science and Technology

Course pages 2018–19

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 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.

To change the print mode from iterated arrows to the fat brackets shown in the slides, open the Plugins > Plugin Options page of the jEdit window and type the word "brackets" into the print mode box, as shown: