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.
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.