Course pages 2015–16
Interactive Formal Verification
- Practical exercises, both practice and assessed
- The associated Isabelle theory files
The latest version of Isabelle is called Isabelle2015. You will find it at
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.