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 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 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.
• 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 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 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 pvs-file and proved in a gzipped dump-file. The same for mutual exclusion with semaphores: a pvs-file and a gzipped dump-file.