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.

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.

@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/}
}

• CAV95.dvi.gz
• CAV95.ps.gz