Books about ACL2
- How to use ACL2:
Computer-Aided Reasoning: An Approach, Matt Kaufmann,
Panagiotis Manolios, and J Strother Moore,
Kluwer Academic Publishers,
June, 2000. (ISBN 0-7923-7744-3)
- What can be done with ACL2:
Computer-Aided Reasoning: ACL2 Case Studies, Matt Kaufmann,
Panagiotis Manolios, and J Strother Moore (eds.),
Kluwer Academic Publishers,
June, 2000. (ISBN 0-7923-7849-0)
Using the techniques described in these two books, users of the ACL2 system
have modeled and proved properties of hardware designs, microprocessors,
microcode programs, and software. In addition, many theorems in mathematics
and meta-mathematics have been proved with ACL2.
Links
- Computer-Aided Reasoning: An Approach: description, excerpts, errata,
solutions to exercises.
- Computer-Aided Reasoning: ACL2 Case Studies: description, list of contributors, excerpts, errata,
full scripts for case studies, solutions to exercises.
- ACL2 Home Page: tours of the system, documentation, technical papers,
source code, installation guide, mailing lists.
- Ordering Information