PVS is currently available at ENSEIRB-MATMECA on ssh.enseirb-matmeca.fr Linux machine, at the following location
This command actually launches Emacs augmented with PVS commands as a detached process.
PVS can also be installed on a laptop under Linux or Mac OS X (including Lion, with some difficulty though...) and even Windows.
Getting started on a simple exampleIn order to run PVS on this machine, you are advised to take the following steps:
It is convenient to define pvs as a symbolic link in each PVS context (directory), such as intro, you will use for exercises or for your project:
ln -s /usr/local/pvs/5.0/pvs pvsThen you just have to type
from the relevant PVS context (directory), in order to launch PVS from this context.
About dumps and PVS directories
A PVS dump is a unique text file corresponding to a snapshot of all your theories and proofs contained in a PVS directory (also called PVS context, or PVS library). A dump is thus a convenient means of representing the comprehensive state of your theories and proofs in a given directory, and sharing it with other people. There is a "root theory" in every dump: the root theory directly or indirectly imports all other theories. For instance, the first_steps theory in the simple example below imports the propositional and f91 theories among others. Before producing a dump, it is important to type check your root theory; otherwise, your dump will be incomplete.
In this class, we generally use a precise scheme to name a dump:
According to this convention, the above first_steps.dmp.txt PVS dump should rather have been named:
Although it is also possible to produce a more complex dump (called inclusive) representing several directories (libraries), in the case where some libraries depend upon other ones, it is not a good idea in practice: you are advised to produce only simple dumps, not inclusive dumps. Beware of the terminology:
A theory file, such as theory_name.pvs, usually corresponds one and one only theory identified by its name: theory_name; the proofs associated with a theory are automatically stored in a unique file named theory_name.prf. You should not edit proof files.