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

PVS User Group and Tutorial at FM'99 - Programme

			Call for Participation
                     PVS User Group and Tutorial
                      FM'99 - Toulouse, France


In conjunction with FM99, SRI International will present two half day
sessions devoted to the PVS specification and verification system. For
details on PVS, and to download the system, visit the PVS web site at

Tutorial (Wednesday 22 September 14:00 - 17:30)

The tutorial will provide a rigorous introduction to the basic
capabilities of PVS and an overview of its more advanced features, and
will be suitable for both prospective and existing users of PVS. After a
brief overview of the history, goals, technology, status, and applications
of PVS, the body of the tutorial will consist of an extended demo. This
will begin with the basic PVS language and proof constructs and then move
on to more advanced topics such as predicate subtypes, proof strategies,
and combined theorem proving and model checking. The final hour will cover
recent or advanced capabilities such as executable specifications, proof
search, extended decision procedures (including WS1S), and automated

The tutorial will provide prospective users with an appreciation for the
capabilities of PVS and the ability to start using it on their own, while
existing users will gain an introduction to some of its more exotic and
advanced capabilities.

User Group Meeting (Tuesday 21 September 14:00 - 17:30)

The PVS User Group Meeting at FM99 will provide an opportunity to meet
fellow users of PVS, and some of the PVS developers. The user group
meeting is intended as a forum for exchanging experiences, ideas, results,
and libraries, and influencing the future direction of PVS. The meeting
will include:

o Invited Talk: Prof. Amir Pnueli, Weizmann Institute;

o Presentations by PVS Users:

  o "Specification and Verification of ASMs in PVS",
    F. Bartels, A. Dold, H. Pfeifer, H. Rue, M. Stegmller,
    V. Vialard, and F. W. v. Henke (University of Ulm);

  o "Pamela and PVS",
    Bettina Buth (University of Bremen);

  o "Refinement of state-based systems in PVS: A uniform Approach
     based on Final Coalgebras",
    Falk Bartels, Friedrich von Henke (University of Ulm),
    Harald Rue (SRI);

  o "PVS-based Verification of SCR-style Requirements: Experience and Wish List",
    Tae-Ho Kim and Sung-Deok Cha (KAIST);

  o "Towards a Customizable PVS",
    Gerald Lttgen, Csar Muoz (ICASE),
    Ricky Butler, Ben DiVito and Paul Miner (NASA Langley);

o A brief presentation from the developers on new and planned enhancements
  to PVS, with an opportunity for users to provide feedback and wish lists. 

Abstracts for the talks are currently available from:



Registration for the PVS Tutorial or User Group Meeting is free, but you
must also register for the main FM99 conference.  Register by visiting
http://pvs.csl.sri.com/fm99.html or by email to dave_sc@csl.sri.com.