PVS(ID:2724/pvs001)Prototype Verification SystemRelated languages
References: 1 Introduction PVS is a prototype system for writing specifications and constructing proofs. Its development has been shaped by our experiences studying or using several other systems 1 and performing a number of rather substantial formal verifications (e.g., [5,6,8]). PVS is fully implemented and freely available. It has been used to construct proofs of nontrivial difficulty with relatively modest amounts of human effort. Here, we describe some of the motivation behind PVS and provide some details of the system. Automated reasoning systems typically fall in one of two classes: those that provide powerful automation for an impoverished logic, and others that feature expressive logics but only limited automation. PVS attempts to tread the middle ground between these two classes by providing mechanical assistance to support clear and abstract specifications, and readable yet sound proofs for difficult theorems. Our goal is to provide mechanically-checked specifications and proofs that contribute to the social process by which purported theorems come to be discarded or accepted, and designs for critical systems get certified. PVS combines an expressive logic with a powerful but highly interactive proof checker that supports top-down proof exploration and construction. In addition to its proof checker, the PVS system includes a parser, prettyprinter, and typechecker. We describe the PVS logic and proof checker in the following sections. Extract: Influences Lack of space prevents us from discussing or explicitly referencing the many systems and notations that have influenced us in one way or another. These include Affirm, Automath, Ehdm, EKL, EVES, FDM, Gypsy, HOL, IMPLY, IMPS, LCF, LP, Muse, Nqthm, Nuprl, OBJ, Ontic, PC-Nqthm, RAISE, RRL, STP, TPS, Tecton, VDM, Veritas, and Z among others. Most of our ideas can be traced to one or other of these earlier efforts. |