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

Computer-Aided Computing
 by Dr. Natarajan Shankar.

Formal program design methods are most useful when sup ported with suitable mechanization. This need for mechanization has long been apparent, but there have been doubts whether verification technology could cope with the problems of scale and complexity. Though there is very little compelling evidence either way at this point, several powerful mechanical verification systems are now available for experimentation. Using SRI's PVS as one representative example, we argue that the technology of mechanical verification is already quite effective. PVS derives its power from an integration of theorem proving with type checking, decision procedures with interactive proof construction, and more recently, model checking with theorem proving. We discuss these individual aspects of PVS using examples, and motivate some of the challenges that lie ahead.


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