• Top
  • Documentation
    • Xdoc
    • ACL2-doc
    • Recursion-and-induction
    • Loop$-primer
    • Operational-semantics
    • Pointers
    • Doc
    • Documentation-copyright
    • Course-materials
    • Publications
      • Pub-books
      • Pub-papers
        • Pub-programming-languages
        • Pub-processor-models
        • Pub-miscellaneous-applications
        • Pub-logic-and-metamathematics
        • Pub-foundations
        • Pub-floating-point-arithmetic
        • Pub-data-structures
        • Pub-real-arithmetic
        • Pub-overviews
        • Pub-capabilities
        • Pub-model-checking-and-ste
        • Pub-utilities
        • Pub-concurrency
      • Pub-summary
      • Pub-related-web-sites
    • Args
    • ACL2-doc-summary
    • Finding-documentation
    • Broken-link
    • Doc-terminal-test-2
    • Doc-terminal-test-1
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Pub-papers

Pub-overviews

Overviews

• About ACL2
• ACL2 Theorems about Commercial Microprocessors, Bishop Brock, Matt Kaufmann and J Moore, in M. Srivas and A. Camilleri (eds.) Proceedings of Formal Methods in Computer-Aided Design (FMCAD'96), Springer-Verlag, pp. 275-293, 1996. The paper sketches the system and two industrial applications: the AMD5K86 floating-point division proof and the Motorola CAP DSP model.
• An Industrial Strength Theorem Prover for a Logic Based on Common Lisp Matt Kaufmann and J Moore, IEEE Transactions on Software Engineering 23(4), April 1997, pp. 203-213. We discuss how we scaled up the Nqthm (“Boyer-Moore”) logic to Common Lisp, preserving the use of total functions within the logic but achieving Common Lisp execution speeds, via the introduction of “guards.”
• Hyper-Card for ACL2 Programming by Matt Kaufmann and J Moore. This is a quick reference sheet with lots of hyper-text links to the online documentation. It also contains a gentle introduction to Lisp programming.
• A Computational Logic for Applicative Common Lisp, Matt Kaufmann and J Moore. In: A Companion to Philosophical Logic, D. Jacquette (ed.), Blackwell Publishers, pp. 724-741, 2002.
• Design Goals of ACL2, Matt Kaufmann and J Moore, CLI Technical Report 101, Computational Logic, Inc., 1717 West Sixth Street, Suite 290, Austin, TX 78703, 1994. This is an early report identifying aspects of Nqthm of special concern during the design of ACL2.
• Maintaining the ACL2 Theorem Proving System, Matt Kaufmann and J Strother Moore. Invited talk. Proceedings of the FLoC'06 Workshop on Empirically Successful Computerized Reasoning, 3rd International Joint Conference on Automated Reasoning (G. Sutcliffe, R. Schmidt, and S. Schulz, eds.), CEUR Worksho Proceedings Vol. 192, Seattle, Washington, August 2006.
• Some Key Research Problems in Automated Theorem Proving for Hardware and Software Verification, Matt Kaufmann and J Strother Moore. Revista de la Real Academia de Ciencias (RACSAM), Vol. 98, No. 1, pp. 181--196, 2004. Spanish Royal Academy of Science.
• ACL2 Support for Verification Projects, Matt Kaufmann. Invited talk, Proc. 15th Intl. Conf. on Automated Deduction, ed. C. Kirchner and H. Kirchner, Lec. Notes Artif. Intelligence 1421, Springer-Verlag, Berlin, 1998, pp. 220--238.
• An Industrial Strength Theorem Prover for a Logic Based on Common Lisp, Matt Kaufmann and J Moore). IEEE Transactions on Software Engineering 23, no. 4, April 1997, 203--213.
• Design Goals for ACL2, Matt Kaufmann and J Strother Moore. In proceedings of: Third International School and Symposium on Formal Techniques in Real Time and Fault Tolerant Systems, Kiel, Germany (1994), pp. 92-117. Published by Christian-Albrechts-Universitat.
• Enhancements to ACL2 in Versions 6.2, 6.3, and 6.4, Matt Kaufmann and J Strother Moore. Here is a link to the slides from that talk at ACL2 Workshop 2014.
• Enhancements to ACL2 in Versions 5.0, 6.0, and 6.1, Matt Kaufmann and J Strother Moore. Talk given at ACL2 Workshop 2013.