Computer Laboratory

Course material 2010–11

Interactive Formal Verification

Principal lecturer: Dr Tjark Weber
Convenor: Prof Mike Gordon
Taken by: MPhil ACS

Syllabus

Slides 1. Introduction 2. Theories 3. Proof 4. Advanced Recursion 5. Logic 6. Sets 7. Inductive Definitions Review: Lectures 1-7 8. Operational Semantics 9. Presenting Theories 10. Structured Proofs 11. Structured Induction Proofs Guest Lecture: Automated Theorem Proving 12. Modelling Hardware (last year's slides)

Practical Exercises:
Week 1: Exercises1.pdf Exercises1.thy   Solution1.pdf Solution1.thy
Week 2: Exercises2.pdf Exercises2.thy   Solution2.pdf Solution2.thy
Week 3: Exercises3.pdf Exercises3.thy   Solution3.pdf Solution3.thy
Week 4: Exercises4.pdf Exercises4.thy   Solution4.pdf Solution4.thy
more exercises

This lecture course introduces interactive formal proof using Isabelle. The lecture notes consist of copies of the slides, some of which have brief remarks attached. Extensive Isabelle documentation is available. The most important single manual is the Tutorial on Isabelle/HOL. Reading the Tutorial is an excellent way of learning Isabelle in depth. However, the Tutorial is a little outdated; although its details remain correct, it presents a style of proof that has become increasingly obsolete with the advent of structured proofs and ever greater automation. These lecture notes take a different approach and refer you to specific sections of the Tutorial that are particularly appropriate.

Much of the other documentation is only suitable for advanced users. The most useful documents are What's in Main, which lists the main types and functions available in Isabelle/HOL, and the Tutorial on Function Definitions. Other documents, in particular the User's Guide to Sledgehammer, the Tutorial on Type Classes and the Tutorial on Code Generation, often go well beyond what we will cover in this course. The Tutorial on Isar presents a different approach to structured proof; its perspective may be valuable.

You can run Isabelle from a Computer Laboratory Linux workstation using the following command:

    /usr/groups/theory/isabelle/Isabelle/bin/isabelle emacs -p emacs-snapshot

If there are any difficulties, send an e-mail to tw333@cam.ac.uk.

You will probably want to put something in your .profile to shorten this command, either by creating an alias or by augmenting your search path.

This command starts Isabelle with its Proof General user interface, which is based on the text editor Emacs. You will need to learn how to use Emacs. Advanced skill is not necessary, merely the ability to move backward and forward in a file and to insert or delete text. (Learning is not that difficult, especially because the arrow keys and mouse behave more or less as you would expect.) A number of Emacs tutorials can be found on the Internet and may be helpful.

Isabelle is easily installed on UNIX based workstations (including Mac OS X), and with greater effort on Windows using Cygwin. Full instructions are available online.

Important note: the course sessions take place in two different rooms.

  • Mondays, Wednesdays and Fridays at 10 AM in SW01.
  • Fridays at 12 noon are practical sessions in SW02. There will be no lecture, but Dr Weber will be available to lend assistance.