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