[Prev][Next][Index][Thread]

PVS Tutorial/Workshop in Tokyo: April 4, 1996 at Kieo U.(Mita campus)


[------ The Types Forum ------- http://www.dcs.gla.ac.uk/~types ------]




A Tutorial/Workshop on Formal Specification and Verification Using PVS
             Patrick Lincoln, SRI International
         April 4, 1996 at Kieo University (Mita Campus)
              Room 102, Building 1
             9.30am to 4pm (with a break for lunch)
   [Organized with the kind help of Prof. Mitsu Okada and the
               co-organizers of Linear '96]

PVS (Prototype Verification System) is a mechanized tool for formal
specification and verification of safety critical systems that has been
developed by researchers at the SRI International computer science
laboratory.  The PVS system integrates a number of advanced capabilities
for specification and verification such as induction, rewriting, linear
arithmetic, Boolean simplification, and symbolic model checking within
a highly interactive framework.  It has been applied to several hard
problems in fault-tolerant and real-time algorithms, hardware
verification, and computing.  Formally verified examples include various
fault-tolerant agreement and diagnosis algorithms, the correctness of
commercial-scale processor designs, and more recently, the design of an
SRT divider.  PVS is available from SRI and various mirror sites in
England, France, and Germany by anonymous FTP.  See the web site:
http://www.csl.sri.com/pvs.html for details.

The tutorial is open to any interested participant.  This tutorial will
review the basic capabilities of PVS and provide glimpses of several of
its more advanced features.  The purpose of the tutorial is give
attendees an appreciation for the scope and power of modern mechanizations
of formal methods, and for the opportunities these create for efficient
and effective use of formal methods in a variety of application areas.
The tutorial will be conducted as a live demonstration using a workstation
with projection capabilities.  The tutorial will be conducted by Patrick
Lincoln, who is a member of the PVS development team at SRI and an expert
PVS user.

There will be time for short presentations on any topic of relevance to
mechanized formal methods in general, or PVS in particular.  Please
send email to shankar@csl.sri.com if you would like to make such a
presentation.    

The topics covered in the tutorial include:
  * Some introductory tutorial examples
  * The PVS Language: Type System, Definitions, the prelude library,
    Parametric theories, Recursive datatypes, Tables, 
    Inductive relations, Libraries.
  * The PVS Prover: Propositional Logic, Quantification,
    Decision Procedures, Rewriting, Proof Strategies,
    Induction, BDD-based symbolic model checking.
  * Advanced Applications

There is no registration for this tutorial.  For more details,
please send email to shankar@csl.sri.com or phone Mr. Eiji Kitahara (SRI,
Tokyo) at  +(81) 03-3505-8914; Fax +(81) 03-3505-8920.