Course pages 2012–13

Interactive Formal Verification

• Practical exercises, both practice and assessed
• The associated Isabelle theory files
  1. replace
  2. powSum
  3. Tree (Clarification: Task 5 requires you to write a delete function for a binary search tree, taking advantage of the ordering)
  4. FSM (Clarification: In Task 3, you may use a specific type of states when defining SingStr.)

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. The system has been revamped for Isabelle2013, so please use that. You will find it at /usr/groups/theory/isabelle/Isabelle2013/. With this approach, you can create a directory for an exercise by typing

  /usr/groups/theory/isabelle/Isabelle2013/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/Isabelle2013/bin/isabelle build -D Paulson1

You will find more information in the 2013 version of 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. Another complication is that you may notice slight incompatibilities between Isabelle2012 and Isabelle2013.

A simple alternative to all this, involving Proof General, is mentioned on page 1 of the exercises handout.

For further practice, here are many more Isabelle/HOL exercises!