"N, V, Z(MSM 262200012)" . "[1368E605397F]" . "Protocol Proving Using PVS: A Case Study" . "1"^^ . "Prototype Verification System (PVS) is a popular verification tool for writing formal specification and checking formal proofs. It consists of a specification language integrated with support tools and a theorem prover. This paper shows its application on the class of high-level communication protocols. Case study is demonstrated on a simple protocol for user database access. The paper discusses problems of formal specification of communication protocols, its representation using PVS language and a set of properties to be proved."@en . "2001-05-09+02:00"^^ . "26230" . . "1"^^ . "7"^^ . . "Prototype Verification System (PVS) is a popular verification tool for writing formal specification and checking formal proofs. It consists of a specification language integrated with support tools and a theorem prover. This paper shows its application on the class of high-level communication protocols. Case study is demonstrated on a simple protocol for user database access. The paper discusses problems of formal specification of communication protocols, its representation using PVS language and a set of properties to be proved." . . "Hradec n/M" . . . "80-85988-57-7" . "Protocol Proving Using PVS: A Case Study"@en . "Protocol Proving Using PVS: A Case Study"@en . . "formal verification, PVS, communication protocol"@en . . "Hradec nad Moravic\u00ED" . "Protocol Proving Using PVS: A Case Study" . . "Neuveden" . . "Matou\u0161ek, Petr" . "693496" . . "RIV/00216305:26230/01:PU28657" . . "Proceedings of the 35th Spring Conference: Modelling and Simulation of Systems - MOSIS'01" . . . . . "RIV/00216305:26230/01:PU28657!RIV11-MSM-26230___" . . . .