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

Combining Theorem Proving and Model Checking through Symbolic Analysis
 by Dr. Natarajan Shankar.

Lecture Notes in Computer Science, Number 1877.
From CONCUR'00: Concurrency Theory.
Springer-Verlag, State College, PA.
August, 2000.
Pages 1–16.
© Copyright Springer-Verlag.


Abstract
Automated verification of concurrent systems is hindered by the fact that the state spaces are either infinite or too large for model checking, and the case analysis usually defeats theorem proving. Combinations of the two techniques have been tried with varying degrees of success. We argue for a specific combination where theorem proving is used to reduce verification problems to finite-state form, and model checking is used to explore properties of these reductions. This decomposition of the verification task forms the basis of the Symbolic Analysis Laboratory (SAL), a framework for combining different analysis tools for transition systems via a common intermediate language. We demonstrate how symbolic analysis can be an effective methodology for combining deduction and exploration.
BibTEX Entry
@inproceedings{concur2000,
    AUTHOR = {Natarajan Shankar},
    TITLE = {Combining Theorem Proving and Model Checking through Symbolic Analysis},
    BOOKTITLE = {{CONCUR'00:} Concurrency Theory},
    YEAR = {2000},
    SERIES = {Lecture Notes in Computer Science},
    NUMBER = {1877},
    PAGES = {1--16},
    ADDRESS = {State College, {PA}},
    MONTH = {aug},
    PUBLISHER = {Springer-Verlag},
    URL = {http://www.csl.sri.com/papers/concur2000/},
    COPYRIGHT = {Springer-Verlag}
}
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