Computer-Aided Reasoning: ACL2 Case Studies

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.