User Group Meeting

PVS Specification and Verification System

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

Towards A Customizable PVS

Gerald LŸttgen, CŽsar Mu–oz
{luettgen, munoz}@icase.edu
Institute for Computer Applications in Science and Engineering (ICASE)
Mail Stop 132C, 3 West Reid Street, NASA Langley Research Center, Hampton VA 23681-2199

Ricky Butler, Ben Di Vito, Paul Miner
{r.w.butler, b.l.divito, p.s.miner}@larc.nasa.gov
Mail Stop 130, 1 South Wright Street, NASA Langley Research Center, Hampton VA 23681-2199

NASA Langley is a long-time user of the verification system PVS, developed and maintained by SRI International. Our experiences with PVS show that it is a well-performing theorem-proving tool, provided that the application under consideration can be tailored to PVS's problem solving style. Unfortunately, tailoring applications is difficult in practice, leading to a desire for tool customization. This desire is shared by researchers at ICASE, whose main interest is the development of new verification technologies, especially heterogeneous techniques combining theorem proving, model checking, and type checking. Currently, the main means for customizing PVS is a rudimentary ability for writing application-specific proof strategies. In the following, we suggest several improvements regarding this issue and hope that these might start a fruitful discussion about how to achieve greater customizability in PVS in the short term. We conclude this abstract by stating some of our thoughts on more long-term goals, namely, transitioning from customizability to extensibility by shifting to a more open system architecture.

PVS's current abilities for customization to specific application scenarios are limited to adjusting some environmental variables, pre-loading particular theories, and defining new proof strategies from existing ones. Although PVS provides some simple proof combinators (also called tacticals in other systems), it is often necessary to write new strategies using a PVS-augmented form of the Lisp language. Unfortunately, the lack of documentation poses serious difficulties. The primary problem is access to the current proof context within PVS, including sequents, terms contained within them, and type information about such terms. Moreover, granting strategies raw access to sequents could lead to a breach of soundness. We therefore advocate a simple, clean, well-documented API for writing strategies. Such an API should make data structures representing proof contexts transparent, should enable access to the type checker, and should guarantee that strategies are added conservatively to the system.

Two choices for a strategy language seem possible: (1) an external language, such as Lisp, as is the case in the actual PVS implementation, or (2) the PVS language itself, or an executable subset of it, with a few, appropriately chosen, new language constructs. Our feeling is that the first choice is favorable when concerned with the efficiency of the theorem prover. The second option seems to be more elegant and powerful. In particular, it can be used to advantage in ensuring the soundness of user-supplied strategies.

The flexibility and power of a strategy language is also determined by the level on which system internals, such as decision procedures, can be accessed. We strongly recommend making decision procedures accessible to the strategy language by adding appropriate interfaces. We believe that the benefits of the suggested enhancements are immediate. We just mention that a more customizable PVS - which should be possible to achieve with modest resources - supports the tool's adaptability to a much broader range of industrial and academic applications.

Customizability is a first step towards a (user) extensible PVS. More steps must follow in the long term, most of which demand significant changes in PVS's monolithic architecture. Of special importance to us are: (1) a further parameterization of essential PVS components in order to reason about user-supplied notions of congruence, (2) the ability to conveniently add new decision procedures or heuristics, such as for non-linear arithmetic expressions, and (3) the user customization of the rich PVS language and type system by identifying sublanguages, e.g., a sublanguage restricted to finite types, first-order logic, or executable subsets of the PVS language, or a sublanguage specifically targeted towards writing proof strategies. Additional system features will undoubtedly be needed to support these ideas, such as user interface utilities, public data/file formats for intermediate results, and pedigree tracking so that users know which components were used and who produced them.

We are aware of the very delicate theoretical and technical issues behind our proposal. However, a more open PVS architecture is a prerequisite for research groups outside SRI being able to make useful contributions to the PVS community. While the PVS language remains powerful and elegant, analysis techniques within the Formal Methods domain are becoming increasingly heterogeneous, drawing from a wide spectrum of specialized ideas. PVS would make an ideal flagship, but it cannot be the whole fleet. It would be wise to outfit PVS with a highly flexible means of cooperation, so that we might all enjoy a smoother cruise.