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

Integrated Formal Verification: Using Model Checking With Automated Abstraction, Invariant Generation, and Theorem Proving
 by Dr. John Rushby.

Lecture Notes in Computer Science, Volume 1680.
From Theoretical and Practical Aspects of SPIN Model Checking: 5th and 6th International SPIN Workshops.
Edited by D. Dams, R. Gerth, S. Leue and M. Massink.
Springer-Verlag, Trento, Italy, and Toulouse, France.
July/Sept, 1999.


Abstract
Mechanized formal methods that use both model checking and theorem proving seem to hold most promise for the future. Effective use of both technologies requires they be recast as methods for calculating properties of specifications, rather than merely verifying them. The most valuable properties are those that contribute to the development of invariants and property-preserving abstractions. We outline an architecture for verification tools based on iterated use of such capabilities.
BibTEX Entry
@INPROCEEDINGS{Rushby99:SPIN,
    AUTHOR = {John Rushby},
    TITLE = {Integrated Formal Verification: Using Model Checking With Automated Abstraction, Invariant Generation, and Theorem Proving},
    VOLUME = {1680},
    YEAR = {1999},
    MONTH = {July/Sept},
    ADDRESS = {Trento, Italy, and Toulouse, France},
    URL = {http://www.csl.sri.com/papers/spin99/},
    SERIES = {Lecture Notes in Computer Science},
    BOOKTITLE = {Theoretical and Practical Aspects of {SPIN} Model Checking: 5th and 6th International {SPIN} Workshops},
    PUBLISHER = {Springer-Verlag},
    EDITOR = {{D.} Dams and {R.} Gerth and {S.} Leue and {M.} Massink}
}
Files
 













 

About Us  |  R&D Divisions  |  Careers  |  Newsroom  |  Contact Us
© 2024 SRI International 333 Ravenswood Avenue, Menlo Park, CA 94025-3493
SRI International is an independent, nonprofit corporation. Privacy policy