Date: May 10, 2002, 11am

Place: Columbia

This talk will describe some work in progress aimed at increasing the reach of verification methods by combining the deductive power of finite-state model checking with the expressiveness and flexibility of general-purpose theorem proving. We describe a framework that integrates two model checking algorithms, symbolic trajectory evaluation and symbolic model checking for LTL, into a higher order logic theorem-proving context.

The formal basis of the integration is a semantic embedding into higher-order logic of the LTL formalisms of the model checkers, a technique well-known in theorem proving. A more novel aspect is the use of "reflection", the process by which a logical connection is made between the language and meta-language of the theorem prover. The talk will sketch the motivation for and pragmatic advantages of this idea.

This is joint work with John O'Leary at Intel's Strategic CAD Labs.