The Role of Automated Reasoning in Integrated System Verification Environments
Donald I. Good, Matt Kaufmann, J Strother Moore · 2006
This paper focuses on "system verification," the activity of mechanically proving properties of computer systems. Distinguishing characteristics of systems include their large size, their multiple layers of abstraction, and their frequent concern with multiple programming languages and, more generally, multiple models of computation. System verification systems require supreme integration of their component parts. To reason formally about systems one must be able to reason about the relations between its disparate modules, layers of abstraction, and various models of computation. Facilitating system verification is, we believe, the underlying theme of this "Workshop on the Effective Use of Automated Reasoning Technology in System Development." We address that theme explicitly in this paper. We make an important, often overlooked, but essentially trivial point: to reason formally about the relations between various ideas, those ideas must be formalized. However, the popular approach to ...