Computer Laboratory

Course pages 2014–15

Interactive Formal Verification

The latest version of Isabelle is called Isabelle2014. You will find it at /usr/groups/theory/isabelle/Isabelle/.

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.