Additional resources (talks, academic papers, a dissertation) for learning about GL.

Besides this xdoc documentation, most GL users will probably want to be aware of at least the following resources:

- Sol Swords and Jared Davis. Bit-Blasting ACL2 Theorems. In ACL2 Workshop 2011. November, 2011. EPTCS 70. Pages 84-102.
- This is an approachable, user-focused introduction to GL as of 2011, which also contains many pointers to related work. It's probably a good idea to read this first, noting that a few details have changed. Much of this paper has now been incorporated into this xdoc documentation.
- Sol Swords. A Verified Framework for Symbolic Execution in the ACL2 Theorem Prover. Ph.D. thesis, University of Texas at Austin. December, 2010.
- This is the most comprehensive guide to GL's internals. It covers tricky
topics like the handling of
*if*statements and the details of BDD parametrization. It also covers the logical foundations of GL, such as correctness claims for symbolic counterparts, the introduction of symbolic interpreters, and the definition and verification of the GL clause processor. Some topics are now somewhat dated, but it is good general background for anyone who wants to extend GL. - The documentation for hons-and-memoization.
- GL makes heavy use of hash consing and memoization. GL users will likely want to be aware of the basics of hons-and-memoization, and of commands like hons-summary, hons-wash, and set-max-mem.

- Jared Davis and Sol Swords. Verified AIG Algorithms in ACL2. In ACL2 Workshop 2013. May, 2013. EPTCS 114. Pages 95-110.
- This is a more recent paper that's not especially focused on GL, but which covers aignet and satlink, which can be used by GL in its new gl-satlink-mode. Many problems that are difficult to solve using ubdds can be solved using satlink.
- Sol Swords and Warren A Hunt, Jr. A Mechanically Verified AIG to BDD Conversion Algorithm. In ITP 2010, LNCS 6172, Springer. Pages 435-449.
- This is an older paper about the details of the
bddify algorithm that is used as the engine for gl-aig-bddify-mode.

GL has been used at Centaur Technology to verify RTL implementations of floating-point addition, multiplication, and conversion operations, as well as hundreds of bitwise and arithmetic operations on scalar and packed integers. Some papers describing some of this work include:

- Anna Slobodova, Jared Davis, Sol Swords, and Warren A. Hunt, Jr. A Flexible Formal Verification Framework for Industrial Scale Validation. In Memocode 2011, IEEE. Pages 89-97.
- Warren A. Hunt, Jr., Sol Swords, Jared Davis, and Anna Slobodova.
*Use of Formal Verification at Centaur Technology*. In David Hardin, editor, Design and Verification of Microprocessor Systems for High-Assurance Applications, Pages 65-88. Springer, 2010.

GL is the successor of Boyer and Hunt's **G** system, the best
description of which may be found in:

- Robert S. Boyer and Warren A. Hunt, Jr. Symbolic Simulation in ACL2. In ACL2 Workshop 2009, ACM, 2009. Pages 20-24.

The name, GL, its name stands for *G in the Logic*. The G system was
written as a raw Lisp extension of the ACL2 kernel, so using it meant trusting
this additional code. In contrast, GL is implemented as ACL2 books and its
proof procedure is formally verified by ACL2, so the only code we have to trust
is in ACL2, including its hons-and-memoization features.