Integrating Model Checking and Theorem Proving for Industrial Hardware Verification in a Reflective Functional Language

Photograph of Tom Melham

Tom Melham

(Oxford)

Forte is a formal verification system developed by Intel's Strategic CAD Labs for applications in hardware design and verification. Forte integrates model checking and theorem proving within a functional programming language, which both serves as an extensible specification language and allows the system to be scripted and customized. Forte's functional programming language is also the underlying term language for the higher order logic of its theorem prover.

The latest version of this language, called reFLect, has quotation and antiquotation constructs similar to those in LISP, but typed. These build and decompose expressions in the language itself and provide a combination of pattern-matching and metaprogramming features tailored especially for the Forte applications. The addition of some reflection principles in the higher order logic based on reFLect also provides a framework for making a logically principled connection between theorems in higher-order logic, program execution in the reFLect language, and the results of model checking verifications.

This talk will give an account of the reFLect functional language and its role in Forte.

This is joint work with Jim Grundy, Sava Kristic, and John O'Leary of Intel Corporation.
Tuesday 8th February 2005, 14:00
Robert Recorde Room
Department of Computer Science