Course pages 2013–14

Interactive Formal Verification

• Practical exercises, both practice and assessed
• The associated Isabelle theory files
  1. replace
  2. powSum
  3. Taut
     (Clarification: normal form should also eliminate TRUE and FALSE from conditions. The condition of a normalised if-expression should only be a variable.)
  4. Binomial

The latest version of Isabelle is called Isabelle2013-2. 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.