A Tutorial on an Interactive Proof Assistance Tool PVS.

DOI Web Site 7 References
  • TAKAKI Osamu
    Faculty of Science, Kyoto Sangyo University
  • WATANABE Hiroshi
    Research Center for Verification and Semantics (CVS), National Institute of Advanced Industrial Science and Technology (AIST)
  • TAKEYAMA Makoto
    Research Center for Verification and Semantics (CVS), National Institute of Advanced Industrial Science and Technology (AIST)

Bibliographic Information

Other Title
  • 続・システム検証の科学技術　　対話型証明支援ツールＰＶＳの紹介
  • チュートリアル 対話型証明支援ツールPVSの紹介
  • チュートリアル タイワガタ ショウメイ シエン ツール PVS ノ ショウカイ

Search this article

Description

The purpose of this paper is to introduce PVS, that is one of proof assistant systems, and the application example. In Sections 1 and 2, we roughly explain PVS and the work flow. In Sections 3 and 4, we review basic concepts of types and proofs that are the most important concepts in PVS. In Section 5, we introduce an application of PVS, that is, we introduce a short program that classifies and interprets certain strings, and verify the program via PVS.

Journal

  • Computer Software

    Computer Software 22 (3), 37-57, 2005

    Japan Society for Software Science and Technology

References(7)*help

See more

Details 詳細情報について

Report a problem

Back to top