Randal E. Bryant

Randal E. Bryant -- Caltech, then Carnegie Mellon. **Seventeen records** as of 2026-09-27, almost all of them his alone, and they form the most complete single line in this corpus: from a simulator for MOS circuits to the data structure that made symbolic verification tractable, and on to the theory behind an industrial verification flow and, thirty-five years later, to making that data structure emit checkable proofs of its own answers. Every step is held as a primary source and all but one is readable.

Seven were added in September 2026 from Bryant's own publication index at www.cs.cmu.edu/~bryant/pubdir/, which is reachable and lists a PDF after most entries: **bryant1981switchlevel** (the 1981 MIT doctoral thesis, which moves the line's start three years earlier than the 1984 paper usually cited), **bryant1990ternary** and **bryant1991formal** (the theory and the announcement of symbolic trajectory evaluation), **bryant1991memory**, **bryant1991extraction**, **bryant1991complexity** (the exponential lower bound on OBDD representations of multiplier bits) and **bryant2021dual**.

**Do not audit this set with the set get command.** It lists 8 of the 17; the queue's own count is the reliable one. See issue #185. The list below is the set's origin and not its contents.

1982 bryant1982mossim MOSSIM II, the switch-level simulator, as a user's manual 1984 bryant1984switchlevel the model behind it: charge storage nodes, resistive switches, three values 1985 bryant1985symbolic MOSSYM: set an input to a Boolean variable, and one run replaces exponentially many 1986 bryant1986graphbased ordered binary decision diagrams 1987 bryant1987algorithmic switch networks as sparse Boolean equation systems, solved by Gaussian elimination 1987 bryant1987boolean the companion: that analysis matches MOSSIM II, bidirectionality and X included 1987 bryant1987cosmos COSMOS, the compiler that does it in practice 1991 bryant1991methodology the argument that a logic simulator can prove correctness, because X stands for all unknowns 1995 seger1995formal with Seger: symbolic trajectory evaluation, the state space ordered by information content 2018 bryant2018binary his own retrospective on binary decision diagrams

**The ordering corrects a story the corpus had backwards.** It is natural to assume the data structure came first and found applications. It did not. bryant1985symbolic verifies MOS circuits symbolically a year before OBDDs are published, using what it calls only "heuristically efficient Boolean function manipulation algorithms". The *use* is established first; bryant1986graphbased then supplies the representation that makes it cheap.

**He is unusually candid about the limits of his own results**, and the corpus should quote him on them. bryant1986graphbased states that choosing a good variable ordering is coNP-complete and that an appendix proves **integer multiplier outputs grow exponentially for every ordering**. bryant1987boolean gives the analysis as O(n^3) worst case, O(n) for all but dense pass-transistor networks. bryant1984switchlevel's model, he says, "describes the electrical behavior in a highly idealized way". Each result arrives with the class of cases where it fails already named.

**The thread that runs through all of it is a single trick, generalised twice.** In the switch-level model the third value X stands for an unknown. bryant1991methodology turns that into an argument: because X stands for *every* unknown assignment at once, one simulation run discharges an exponential set of cases, so a simulator can prove things. seger1995formal replaces the single extra value with a state space ordered by information content, in which elements represent *sets* of states, and proves that every trajectory formula has a unique weakest satisfying trajectory. X is the two-element case of that ordering. Thirty-four years, one idea, three levels of generality.

**Where the corpus meets him from outside.** burch1994automatic cites his tradition's neighbours rather than him, but shares the conviction that decision procedures beat hand-guided proof; ebergen1989translating and bryant1987algorithmic both date their subject to Shannon's 1938 relay paper, from schools with no other common reference; and gupta2014formally is Intel's deployment of seger1995formal's technique two decades later.

**On the copies.** bryant1982mossim is a scan and unreadable by extraction; bryant1987cosmos, bryant1987boolean, bryant1987algorithmic and seger1995formal use type 3 fonts and yield mojibake, so all four are filed with a zero word count and must be read by rendering. They came from his own publications index at Carnegie Mellon, which lists 141 files and answers reliably. A caution recorded there: each link on that page **follows** the citation it belongs to, so text after a link describes the next entry.