
An Integration of ModelChecking with Automated Proof Checking
by Dr. Natarajan Shankar, S. Rajan & M.K. Srivas.
Lecture Notes in Computer Science, Volume 939. From ComputerAided Verification, CAV '95. Edited by Pierre Wolper. SpringerVerlag, Liege, Belgium. June, 1995. Pages 84–97.
Abstract
Although automated proof checking tools for generalpurpose 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 finitestate 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 BDDbased model checker for
the propositional mucalculus 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.
BibT_{E}X Entry
@inproceedings{Rajan95:CAV,
AUTHOR = {{S.} Rajan and {N.} Shankar and {M.K.} Srivas},
TITLE = {An Integration of ModelChecking with Automated Proof Checking},
BOOKTITLE = {ComputerAided Verification, {CAV} '95},
YEAR = {1995},
EDITOR = {Pierre Wolper},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {939},
PAGES = {8497},
ADDRESS = {Liege, Belgium},
MONTH = {jun},
PUBLISHER = {SpringerVerlag},
URL = {http://www.csl.sri.com/papers/cav95/}
}
Files

