Integrated circuit shop simulation for capacity planning and scheduling. - Dennis D. Newhart; John W. O'Leary (WSC, 1971)

HML: A Hardware Description Language Based on Standard ML. - John W. O'Leary; Mark H. Linderman; Miriam Leeser; Mark D. Aagaard (CHDL, 1993)

Non-Restoring Integer Square Root: A Case Study in Design by Principled Optimization. - John W. O'Leary; Miriam Leeser; Jason Hickey; Mark D. Aagaard (TPCD, 1994)

Verification of a subtractive radix-2 square root algorithm and implementation. - Miriam Leeser; John W. O'Leary (ICCD, 1995)

Verification of All Circuits in a Floating-Point Unit Using Word-Level Model Checking. - Yirng-An Chen; Edmund M. Clarke; Pei-Hsin Ho; Yatin Vasant Hoskote; Timothy Kam; Manpreet Khaira; John W. O'Leary; Xudong Zhao 005 (FMCAD, 1996)

Xs are for Trajectory Evaluation, Booleans are for Theorem Proving. - Mark D. Aagaard; Thomas F. Melham; John W. O'Leary (CHARME, 1999)

A Methodology for Large-Scale Hardware Verification. - Mark D. Aagaard; Robert B. Jones; Thomas F. Melham; John W. O'Leary; Carl-Johan H. Seger (FMCAD, 2000)

Practical Formal Verification in Microprocessor Design. - Robert B. Jones; John W. O'Leary; Carl-Johan H. Seger; Mark D. Aagaard; Thomas F. Melham (IEEE Des. Test Comput., 2001)

An industrially effective environment for formal hardware verification. - Carl-Johan H. Seger; Robert B. Jones; John W. O'Leary; Thomas F. Melham; Mark D. Aagaard; Clark W. Barrett; Don Syme (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2005)

A reflective functional language for hardware design and theorem proving. - Jim Grundy; Thomas F. Melham; John W. O'Leary (J. Funct. Program., 2006)

Verifying Correctness of Transactional Memories. - Ariel Cohen 002; John W. O'Leary; Amir Pnueli; Mark R. Tuttle; Lenore D. Zuck (FMCAD, 2007)

Extracting models from design documents with mapster. - David James; Tim Leonard; John W. O'Leary; Murali Talupur; Mark R. Tuttle (PODC, 2008)

Protocol verification using flows: An industrial experience. - John W. O'Leary; Murali Talupur; Mark R. Tuttle (FMCAD, 2009)

Model Checking Transactional Memory with Spin. - John W. O'Leary; Bratin Saha; Mark R. Tuttle (ICDCS, 2009)

ATLAS: Automatic Term-level abstraction of RTL designs. - Bryan A. Brady; Randal E. Bryant; Sanjit A. Seshia; John W. O'Leary (MEMOCODE, 2010)

Relational STE and theorem proving for formal verification of industrial circuit designs. - John W. O'Leary; Roope Kaivola; Tom Melham (FMCAD, 2013)

Modeling Algorithms in SystemC and ACL2. - John W. O'Leary; David M. Russinoff (ACL2, 2014)