M. Kaufmann, P. Manolios, J S. Moore, Computer-Aided
Reasoning: ACL2 Case Studies, Kluwer Academic Publishers, 2000.
Relevance: tutorial examples of ACL2 applications
This book is a companion to bib::kmm00a. It contains fourteen articles by ACL2 experts, explaining how they formalized and solved fourteen different problems. It also includes exercises.