Theorem Proving with PVS
The main source for the theorem prover PVS
A list of available notes:
- A home-grown 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 undump-pvs-files, 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 control-c control-p 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
- 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 well-known 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 controle-c control-p t. Look at the TCCs generated by
control-c control-q s.
dumpfile of binsearch
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 dump-file into your system,
call PVS, and then in the pvs-menu 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
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
pvs-file and proved in a gzipped
The same for mutual exclusion with semaphores: a
pvs-file and a gzipped
Comments and questions are welcome.
Last modified: Fri Nov 19 16:44:49 CET 2010
Wim H. Hesselink,