Theorem Proving with PVS
The main source for the theorem prover PVS
A list of available notes:
 A homegrown rudimentary
PVS manual. Read this first and try to make sense of it.
 As a first exercise in theorem proving, we use the theory on the
transitive closure of a binary relation contained in the file
dumptrans. If you have pvs working, you can use the PVS menu, go
to Files and Theories, goto undumppvsfiles, undump "dumptrans", and
load the resulting file "trans1.pvs" in the emacs window of PVS. The
file defines the transitive closure of a binary relation. The first
lemma is that the transitive closure is always reflexive. This lemma
has been proved for you. Type controlc controlp x, and you can
replay the proof. Then try to prove the remaining three lemmas
proposed. Finally, modify the file by adding your name as one of the
contributors and extend it with a lemma as suggested at the end of the
file.
 The file
arithDump contains a theory with three recursive definitions and
two inductive proofs. It proves that the sum of subsequent odd numbers
is a square, and it proves the wellknown expression for the sum of a
geometric series. Load it on your system, undump it with PVS, load the
specification file "arithsquare.pvs" in PVS, and prove the whole
theory with controlec controlp t. Look at the TCCs generated by
controlc controlq s.
 The
dumpfile of binsearch
contains a
theory for a binary search program and a
theory for the semantics of sequential programs with Hoare
triples, together with proofs of correctness of both theories. If
you only want to read the theories, inspect the PVS files. If you want
to see how the proofs are done, load the dumpfile into your system,
call PVS, and then in the pvsmenu under "files and theories" use the
item "undump" to undump this file. You then also find auxiliar
theories more_floor and swap.
 The importance of TCCs (type correctness conditions) is illustrated by
the dumpfile
unsoundRec.dump. This contains an unsound recursive definition and uses it
to prove false. When you finally ask PVS what has been proved, you find
an unprovable TCC.

A set of exercises about the correctness of sequential programs.

The correctness of Peterson's mutual exclusion program is specified in a
pvsfile and proved in a gzipped
dumpfile.
The same for mutual exclusion with semaphores: a
pvsfile and a gzipped
dumpfile.
Comments and questions are welcome.
Last modified: Fri Nov 19 16:44:49 CET 2010
Wim H. Hesselink,
email: w.h.hesselink@rug.nl