The Prototype Verification System (PVS) was developed as a research tool for exploring techniques of specification and theorem proving. PVS was made freely available in 1993, and has been steadily growing in popularity, as witnessed by the hundreds of members of the PVS mailing list and the increasing number of papers that reference it [2]. As expected for a system of this size and complexity, various versions and patches have been released since the original distribution. However, while new releases have corrected problems and added new features, they have occasionally introduced errors that cause exist ing specifications and proofs to fail. Therefore, we have developed batch and validation facilities within PVS that makes it easy to rerun system commands and compare the results to earlier runs, and have put together the foundations for a validation suite. This provides the foundation for rigorous regression testing that will be applied to future PVS releases.

• pvs-batch.dvi
• pvs-batch.ps