Computer Laboratory

Course pages 2015–16

Interactive Formal Verification

The latest version of Isabelle is called Isabelle2015. You will find it at /usr/groups/theory/isabelle/Isabelle/. The Isabelle website includes extensive documentation and examples, as well as installers for Windows, OS X and Linux.

You may wish to use Isabelle's document preparation system to produce your assessed exercise write-ups. This is not required, but if done well, will earn some of the final 25 marks in the marking scheme. You can create a directory for an exercise by typing

  /usr/groups/theory/isabelle/Isabelle/bin/isabelle mkroot -d Paulson1

This will create a small directory hierarchy where you can insert your Isabelle theories and general LaTeX files. It will also create a file called ROOT, which you must populate with the names of these files. Then you can create a document file by typing the command

  /usr/groups/theory/isabelle/Isabelle/bin/isabelle build -D Paulson1

You will find more information in the Isabelle tutorial. The document preparation system gives you a combination of Isabelle and LaTeX, with the former acting as a preprocessor for the latter; this makes it tricky to diagnose error messages.