1. R. Boulton, A. Gordon, M. Gordon, J. Harrison, J. Herbert & J. Van Tassel (1992): Experience with Embedding Hardware Description Languages. In: International Conference on Theorem Provers in Circuit Design: Theory, Practice and Experience. North-Holland/Elsevier, pp. 129–156.
  2. D. Hardin (2020): Put Me on the RAC. In: ACL2 2020: 16th International Workshop on the ACL2 Theorem Prover and its Applications, Virtual Conference.
  3. W. Hunt, S. Swords, J. Davis & A. Slobadova (2010): Use of Formal Verification at Centaur Technology. In: David S. Hardin: Design and Verification of Microprocessor Systems for High-Assurance Applications. Springer, pp. 65–88, doi:10.1007/978-1-4419-1539-9_3.
  4. J. Levine (2009): Flex and Bison. O'Reilly Media.
  5. Mentor Graphics Corp.: Algorithmic C Datatypes. Available at
  6. Mentor Graphics Corp.: Sequential Logic Equivalence Checker.
  7. J. O'Leary & D. Russinoff (2014): Modeling Algorithms in SystemC and ACL2. In: ACL2 2014: 12th International Workshop on the ACL2 Theorem Prover and its Applications, Vienna, doi:10.4204/EPTCS.152.12. Available at
  8. D. Russinoff (2018): Formal Verification of Floating-Point Hardware Design: A Mathematical Approach. Springer.
  9. D. Russinoff, M. Kaufmann, E. Smith & R. Sumners (2005): Formal Verification of Floating-Point RTL at AMD Using the ACL2 Theorem Prover. In: 17th IMACS World Congress: Scientific Computation, Applied Mathematics and Simulation, Paris.
  10. Synopsys, Inc.: Hector.

Comments and questions to:
For website issues: