Integrating Verification Components: The Interface is the Message

---

Authors

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

Abstract

The efforts of researchers over the past 20 years has yielded an impressive array of verification tools. However, no single tool or method is going to solve the verification problem. An entire spectrum of formal methods and tools are needed ranging from test case generators, static analyzers, and type checkers, to invariant generators, decision procedures, bounded model checkers, explicit and symbolic model checkers, and program verifiers. These tools and techniques are used to calculate properties of designs and implementations to varying degrees of assurance. They are also interdependent so that a useful verification system typically combines several of these techniques. Much of our work at SRI over the past 15 years has been focused on tool integration both in terms of building verification tools that have been integrated in other systems, and in integrating tools that others have built into our own systems. This paper reports on the theoretical and practical challenges of building component tools as well as integrating components into a larger system. The practical challenges are mainly in managing the trade-off between efficiency and modularity, whereas the theoretical challenges are in achieving cohesive fine-grained and coarse-grained interaction between specialized components. As a step toward addressing these challenges, we present some principles for designing components and integration frameworks focusing on the interfaces between the two.

gzipped postscript

BibTeX Entry

@inproceedings{dMORRS:MONTERREY04,
  TITLE = {Integrating Verification Components: The Interface is the Message}
  AUTHOR = {Leonardo de Moura and Sam Owre and Harald Rue{\ss} and John Rushby and Natarajan Shankar},
  BOOKTITLE = {Proceedings of Monterrey Workshop},
  YEAR = {2004},
  MONTH = {July}, 
  ADDRESS = {Monterrey, California},
  NOTES = {Status: accepted for publication}
}

---

Harald Ruess: ruess@csl.sri.com