Selected References

• Introductions to ALC2.
  • We recommend that you start with the guided Tours.
  • Design Goals for ACL2 -- an early report identifying aspects of Nqthm of special concern during the design of ACL2.
  • ACL2: An Industrial Strength Version of Nqthm -- 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.
  
  
• Examples of the application of ACL2.
  • A Mechanically Checked Proof of the Correctness of the Kernel of the AMD5K86 Floating-Point Division Algorithm (with Tom Lynch) -- the mathematical details of the floating-point division proof.
  • Interactive Consistency in ACL2 (by Bill Young) -- an ACL2 translation of Rushby's PVS improvement to Bevier and Young's Nqthm formalization of the Pease, Shostak and Lamport Oral Messages (``Byzantine Generals'') problem.
  • The Specification of a Simple Autopilot in ACL2 (by Bill Young) -- an ACL2 translation of Butler's PVS formalization of a simple autopilot.
  • Mechanized Formal Reasoning about Programs and Computing Machines (by Boyer and Moore) -- explains a formalization style which has been extremely successful in enabling mechanized reasoning about programs and machines, illustrated in ACL2.
  
  
• ACL2 Documentation.
  • Overview: we recommend that you start with the guided Tours.
  • ACL2 Documentation -- the complete ACL2 documentation tree in the form of a compressed (gzip'd) postscript file. When uncompressed the documentation is approximately 3.5 megabytes of postscript and prints as an 800 page book. The documentation is most useful in its HTML or Texinfo forms, where the links in it can be browsed interactively. The complete HTML documentation tree is available via the Index below or organized by Major Topics.
  • Index to ACL2 on-line reference.

This page is URL http://www.computationallogic.com/software/caeti/acl2/references.html