Integrating Verification Components

Leonardo de Moura, Sam Owre, Harald Ruess, John Rushby, and Natarajan Shankar

Invited position paper for Verified Software: Theories, Tools, Experiments, Zurich, Switzerland, October 2005

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