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