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

---

Panagiotis Manolios and Sudarshan Srinivasan.
ACL2 2004, Fifth International Workshop on the ACL2 Theorem Prover and Its Applications.

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)