Integrating Verification Components
Leonardo de Moura, Sam Owre, Harald Ruess,
John Rushby, and Natarajan Shankar
Abstract
A number of impressive verification tools and techniques
have been developed over the last few years. These tools
have proved successful in verifying limited classes
of properties or small-scale systems. These verification methods include
test case generation, static analysis, type checking, model checking,
decision procedures, and interactive theorem provers. Effective
large-scale verification requires the careful integration of these
verification tools so that deeper properties of large systems
emerge from the cooperation of a suite of tools. We outline some of
the challenges in achieving a coherent integration of verification
components both at fine-grain and coarse-grain levels.
gzipped postscript,
or
plain postscript
or
pdf
or
crude ascii (for your Palm Pilot)
Slides
gzipped postscript,
or
plain postscript
or
pdf
or
crude ascii (for your Palm Pilot)
BibTeX Entry
TBD
Having trouble reading our papers?
Return to John Rushby's bibliography page
Return to the Formal Methods Program home page
Return to the Computer Science Laboratory home page