Course pages 2014–15

Interactive Formal Verification

• Practical exercises, both practice and assessed
• The associated Isabelle theory files
  1. replace
  2. powSum
  3. FunArray
  4. Binomial
     (this exercise is not the same as last year's, despite having the same name)

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.