Sciweavers

TPHOL
1999
IEEE

Lifted-FL: A Pragmatic Implementation of Combined Model Checking and Theorem Proving

13 years 8 months ago
Lifted-FL: A Pragmatic Implementation of Combined Model Checking and Theorem Proving
Combining theorem proving and model checking o ers the tantalizing possibility of e ciently 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 ( ) as both the meta and object language of theorem proving. This is done by \lifting" , essentially deeply embedding in itself. The approach is a pragmatic solution that provides an e cient and extensible veri cation 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.
Mark Aagaard, Robert B. Jones, Carl-Johan H. Seger
Added 04 Aug 2010
Updated 04 Aug 2010
Type Conference
Year 1999
Where TPHOL
Authors Mark Aagaard, Robert B. Jones, Carl-Johan H. Seger
Comments (0)