User Group Meeting

PVS Specification and Verification System

Dave Stringer-Calvert
Email: dave_sc@csl.sri.com

Note: the links above to http://www.fmse.cs.reading.ac.uk/fm99 are no longer valid

In conjunction with FM99, SRI International presented 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 http://pvs.csl.sri.com.

This page is intended to provide links to further information on the user group presentations, and links to the examples presented during the tutorial.

Tutorial

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

• Invited Talk: Prof. Amir Pnueli, Weizmann Institute;
• Presentations by PVS Users:
  • Specification and Verification of ASMs in PVS,F. Bartels, A. Dold, H. Pfeifer, H. Rue§, M. StegmŸller, V. Vialard, and F. W. v. Henke (University of Ulm);
  • Pamela and PVS, Bettina Buth (University of Bremen);
  • Refinement of state-based systems in PVS: A uniform Approach based on Final Coalgebras, Falk Bartels, Friedrich von Henke (University of Ulm) and Harald Ruess (SRI);
  • PVS-based Verification of SCR-style Requirements: Experience and Wish List", Tae-Ho Kim and Sung-Deok Cha (KAIST);
  • Towards a Customizable PVS, Gerald LŸttgen, CŽsar Mu–oz (ICASE) and Ricky Butler, Ben DiVito and Paul Miner (NASA Langley);