Course material 2010–11

# Interactive Formal Verification

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

**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.