This directory contains examples in PVS. The subdirectories contain documentation and PVS dump files or tar files. Download the tar files or files with extension .dmp into your machine (into a clean directory is best). Tar files can be unpacked in the usual way. For dump files, startup PVS, and give the command M-x undump to recreate the PVS specification and proof files. After typechecking, you can single-step the proofs with M-x step-proof and tab-1. A good place to start is the wift-tutorial.