Course pages 2016–17

Interactive Formal Verification

• Assessed Exercises and Marking Criteria
  This document includes a detailed marking scheme. Note that the first two exercises are for practice only. The latter two determine your overall mark for the course.
• The associated Isabelle theory files replace | powSum | Totient | Euclid

The latest version of Isabelle is called Isabelle2016-1. 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. It is your choice whether to 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

  /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 setup allows you to typeset documents that incorporate the results of a live Isabelle session; on the other hand, errors can be difficult to diagnose.