A Suite of Hard ACL2 Theorems Arising in Refinement-Based Processor Verification

Abstract

We have been using ACL2 to verify pipelined machine models for several years and have compiled a suite of 18 problems that arose in the theorem proving process. We believe that this suite will be useful for the future development of ACL2 because it consists of difficult problems that arise in practice, and furthermore, these problems can be handled efficiently by other methods. For example, ACL2 was able to prove the simplest problem in the suite after 15 1/2 days, but UCLID was able to prove the same theorem in seconds.

PDF (70K)
Postscript (128K)

Last modified: Mon Jun 21 10:56:54 EDT 2004 manolios@cc.gatech.edu

Back to Pete's home page College of Computing