skip to primary navigationskip to content

Course pages 2021–22

Interactive Formal Verification

The latest version of Isabelle is called Isabelle2021. 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 run Isabelle on laboratory machines or your own.

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

  mkdir Paulson1
  cd Paulson1
  /usr/groups/theory/isabelle/Isabelle/bin/isabelle mkroot

This will create a small directory hierarchy within Paulson1 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. From the parent directory, you can create a document file by typing the command

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

For the next exercise you can create Paulson2, etc. You will find more information in the Isabelle tutorial and in the Isabelle System Manual. The document preparation system gives you a combination of Isabelle and LaTeX, with the former acting as a preprocessor for the latter. This setup allows you to typeset documents that incorporate the results of a live Isabelle session; on the other hand, typesetting errors can be difficult to diagnose.