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.

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.

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

• spin99-slides.ps.gz
• spin99.dvi.gz
• spin99.ps.gz