Contents

• Access to PVS at ENSEIRB
• Handouts
• PVS information available at CSL SRI International
• Local ENSEIRB copy of some PVS documents 
• First steps with PVS
• Practical tips
• Proof assistant library
• PVS sessions
• PVS exercises

Access to PVS at ENSEIRB

Back to Top.

Handouts

• Two slide presentations are available:
• PVS language: pdf inanimated or html inanimated or animation (use PowerPoint);
• PVS inference: pdf inanimated or html inanimé or animation (use PowerPoint);
• PVS language  in one html page: language summary;   *** new ***
• PVS proof commands in one html page: proof command summary.       *** new ***

Back to Top.

Local ENSEIRB copy of some PVS documents

• les manuels:
• PVS Language Reference: une description du langage de spécification, le langage utilisé pour écrire des théories;
• PVS Prover Guide: une présentation du système d'inférence PVS et des commandes de preuve disponibles sous Emacs;
• PVS System Guide: une présentation de l'utilisation générale de PVS pour la création, le "type checking" ou la preuve de théorie, l'interface Emacs et les interfaces graphiques;
• une documentation courte en ligne sous l'interface Emacs;
• les papiers scientifiques:
• PVS semantics: une présentation formelle de la sémantique du langage de spécification;
• PVS abstract datatypes: une présentation semi-formelle des types abstraits;
• Subtypes for Specification ...: un article de John Rushby, Sam Owre, N. Shankar dans IEEE Transactions on Software Engineering, Vol 24, N°9, September 1998.

First steps with PVS

1. Démarrez PVS depuis votre répertoire "~username/pvs/intro" en tapant "./pvs";
2. Attendez que PVS soit démarré (il lance une fenetre Emacs et initialise l'environnement), puis vous demande de créer un contexte: acceptez la création de ce nouveau contexte en tapant "yes";
3. Quand le "PVS Welcome buffer" apparait, suivez les indications du fichier "README" de ce niveau.