Integration in PVS: Tables, Types, and Model Checking

Abstract. We have argued previously that the e ectiveness of a veri cation system derives not only from the power of its individual features for expression and deduction, but from the extent to which these capabilities are integrated: the whole is more than the sum of its parts 20,21]. Here, we illustrate this thesis by describing a simple construct for tabular speci cations that was recently added to PVS. Because this construct integrates with other capabilities of PVS, such as typechecker-generated proof obligations, dependent typing, higher-order functions, model checking, and general theorem proving, it can be used for a surprising variety of purposes. We demonstrate this with examples drawn from hardware division algorithms and requirements speci cations.

• Type: Conference
• Year: 1997
• Where: TACAS
• Authors: Sam Owre, John M. Rushby, Natarajan Shankar
• Keywords: Algorithms, Speci Cations, Tabular Speci Cations, TACAS 1997, Veri Cation