SRI Logo
About Us|R and D Divisions|Careers|Newsroom|Contact Us|SRI Home
     
  SRI Logo

Using PVS in Batch Mode
 by Sam Owre.

Abstract
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.
Files
 













 

About Us  |  R&D Divisions  |  Careers  |  Newsroom  |  Contact Us
© 2017 SRI International 333 Ravenswood Avenue, Menlo Park, CA 94025-3493
SRI International is an independent, nonprofit corporation. Privacy policy