Lifted-fl: A pragmatic implementation of combined model checking and theorem proving

Abstract

Combining theorem proving and model checking offers the tantalizing possibility of eficiently reasoning about large circuits at high levels of abstraction. We have constructed a system that seamlessly inte- grates 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 eficient 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.