ACL2 is the latest inception of the Boyer-Moore theorem prover, the 2005 recipient of the ACM Software System Award. In the hands of an expert, it feels like a finely tuned race ...
Peter C. Dillinger, Panagiotis Manolios, Daron Vro...
We describe a tutorial that demonstrates the use of the ACL2 theorem prover. We have three goals: to enable a motivated reader to start on a path towards effective use of ACL2; to...