Abstract Download gzipped postscript Bibtex entry |
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.
Bibtex Entry
@INPROCEEDINGS{aagaard-tphols-99,
AUTHOR = {Aagaard , Mark D. and Jones , Robert B. and Seger , Carl-Johan H. },
TITLE = {Lifted-FL: A Pragmatic Implementation of Combined Model Checking and Theorem Proving},
BOOKTITLE = tphols,
YEAR = {1999},
MONTH = jul,
}
Send questions or comments to
Mark Aagaard
< markaa@swen.uwaterloo.ca
>