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

Theorem Proving: Not an Esoteric Diversion, but the Unifying Framework for Industrial Verification
 by D. A. Cryluk & M. K. Srivas.

Abstract
The effectiveness of hardware verification techniques has increased markedly in the past decade. As hardware verification techniques become increasingly powerful the idea of transitioning verification technology to industry can be taken seriously. Nevertheless, powerful decision procedures that can completely automate the verification of certain types of hardware, whether they are BDD based model-checkers [10] or automatic microprocessor verification tools [4], cannot be adequate on their own for industrial hardware verification. However, a high-level, general-purpose the orem prover with specific capabilities can provide an overall framework in which these tools can be embedded and in which they can then be effectively used for industrial hardware verification.
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