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

An Integration of Model-Checking with Automated Proof Checking
 by Dr. Natarajan Shankar, S. Rajan & M.K. Srivas.

Lecture Notes in Computer Science, Volume 939.
From Computer-Aided Verification, CAV '95.
Edited by Pierre Wolper.
Springer-Verlag, Liege, Belgium.
June, 1995.
Pages 84–97.


Abstract
Although automated proof checking tools for general-purpose logics have been successfully employed in the verification of digital systems, there are inherent limits to the efficient automation of expressive logics. If the expressiveness is constrained, there are useful logic fragments for which efficient decision procedures can be found. The model checking paradigm yields an important class of decision procedures for establishing temporal properties of finite-state systems. Model checking is remarkably effective for automatically verifying finite automata with relatively small state spaces, but is inadequate when the state spaces are either too large or unbounded. For this reason, it is useful to integrate the complementary technologies of model checking and proof checking. Such an integration has to be carried out in a delicate manner in order to be more than just the sum of the techniques. We describe an approach for such an integration where a BDD-based model checker for the propositional mu-calculus has been used as a decision procedure within the framework of the PVS proof checker. We argue that our approach fits in nicely with the design philosophy of PVS of providing highly effective mechanical reasoning capability by using efficient decision procedures as the workhorses of an interactive proof checker.
BibTEX Entry
@inproceedings{Rajan95:CAV,
    AUTHOR = {{S.} Rajan and {N.} Shankar and {M.K.} Srivas},
    TITLE = {An Integration of Model-Checking with Automated Proof Checking},
    BOOKTITLE = {Computer-Aided Verification, {CAV} '95},
    YEAR = {1995},
    EDITOR = {Pierre Wolper},
    SERIES = {Lecture Notes in Computer Science},
    VOLUME = {939},
    PAGES = {84--97},
    ADDRESS = {Liege, Belgium},
    MONTH = {jun},
    PUBLISHER = {Springer-Verlag},
    URL = {http://www.csl.sri.com/papers/cav95/}
}
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