|
|
|---|
|
|
|
|---|
Books Published
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.
Details:
Essential Logic for Computer Science, Rex Page and Ruben Gamboa. ISBN 978-0262039185. MIT Press, 2019.
This book is an introduction to the use of predicate logic and ACL2 for testing and verifying software and digital circuits. It has been used as a textbook in an honors introductory course in computing, and with supplementary materials in a course in discrete mathematics.
A Computational Logic, R. S. Boyer and J S. Moore. Academic Press, New York, 1979. xiv+397. The original Pub source for the book is here. The translation to TeX and pdf was kindly done by Gary Klimowicz. The above book is out of print. The copyright has reverted to the authors.
Boyer and Moore hereby place it in the public domain.
Scalable Techniques for Formal Verification, Sandip Ray. ISBN 978-4419-5997-3. Springer, 2010.
This book explains how to develop customized reasoning tools on top of ACL2. The customized reasoning tools extend ACL2 by significantly automating formal proofs on their target domains, but without requiring any modification to the theorem prover source code.
Design and Verification of Microprocessor Systems for High-Assurance Applications, David S. Hardin, ed. Springer, 2010. Quoting from the abstract:
This book examines several leading-edge design and verification technologies that have been successfully applied to microprocessor systems for high-assurance applications at various levels -- from arithmetic circuits to microcode to instruction sets to operating systems to applications. We focus on recent hardware, software, and system designs that have actually been built and deployed, and feature systems that have been certified at high Evaluation Assurance Levels, namely the Rockwell Collins AAMP7G microprocessor (EAL7) and the Green Hills INTEGRITY-178B separation kernel (EAL6+). The contributing authors to this book have endeavored to bring forth truly new material on significant, modern design and verification efforts; many of the results described herein were obtained only within the past year.
Several chapters in this book describe ACL2 proof developments.
Formal Verification of Floating-Point Hardware Design: A Mathematical Approach, David M. Russinoff. Springer, 2019. In the author's words:
This is the first book to focus on the problem of ensuring the correctness of floating-point hardware designs through mathematical methods. It advances a verification methodology based on a unified theory of register-transfer logic and floating-point arithmetic that has been developed and applied to the formal verification of commercial floating-point units over the course of more than two decades, during which the author was employed by several major microprocessor design companies. The entire theory and all applications reported have been formalized and mechanically verified with ACL2.