Reference:

Mark D. Aagaard, Robert B. Jones, and Carl-Johan H. Seger. Lifted-fl: A pragmatic implementation of combined model checking and theorem proving. In Theorem Proving in Higher-Order Logics. Springer-Verlag, September 1999.

Abstract:

Combining theorem proving and model checking offers the tantalizing possibility of efficiently reasoning about large circuits at high levels of abstraction. We have constructed a system that seamlessly integrates symbolic trajectory evaluation based model checking with theorem proving in a higher-order classical logic. The approach is made possible by using the same programming language (FL) as both the meta and object language of theorem proving. This is done by ``lifting'' FL, essentially deeply embedding FL in itself. The approach is a pragmatic solution that provides an efficient and extensible verification environment. Our approach is generally applicable to any dialect of the ML programming language and any model-checking algorithm that has practical inference rules for combining results.

Download (please read copyright notice):

PostScript (gzipped)
PDF (auto-translated from PS, may have problems)

BibTeX entry:

@InProceedings{AagaardJonesSeger99TPHOLS,
  author    = {Mark D. Aagaard and 
               Robert B. Jones and 
               Carl-Johan H. Seger},
  title     = {Lifted-FL: A Pragmatic Implementation of 
               Combined Model Checking and Theorem Proving},
  booktitle = {Theorem Proving in Higher-Order Logics},
  publisher = {Springer-Verlag},
  month     = {September},
  year 	    = 1999,
}