Computer-Aided Reasoning: ACL2 Case Studies illustrates how the computer-aided reasoning system ACL2 can be used in productive and innovative ways to design, build, and maintain hardware and software systems. Included here are technical papers written by twenty-one contributors that report on self-contained and fully reproducible case studies, some of which are sanitized industrial projects. The papers deal with a wide variety of areas, including floating-point arithmetic, microprocessor simulation, model checking, symbolic trajectory evaluation, compilation, proof checking, real analysis, and several others. The case studies also contain exercises whose solutions are on the Web. In addition, the complete proof scripts necessary to formalize the models and prove all the properties discussed are on the Web.
Lulu Staff has been notified of a possible violation of the terms of our Membership Agreement. Our agents will determine if the content reported is inappropriate or not based on the guidelines provided and will then take action where needed.
Thank you for notifying us. We will email you with the results and/or actions taken as a result of the investigation if you chose to receive confirmation.