| 2013 | FMCAD | Relational STE and theorem proving for formal verification of industrial circuit designs. | John W. O'Leary, Roope Kaivola, Tom Melham |
| 2010 | MEMOCODE | ATLAS: Automatic Term-level abstraction of RTL designs. | Bryan A. Brady, Randal E. Bryant, Sanjit A. Seshia, John W. O'Leary |
| 2009 | FMCAD | Protocol verification using flows: An industrial experience. | John W. O'Leary, Murali Talupur, Mark R. Tuttle |
| 2009 | ICDCS | Model Checking Transactional Memory with Spin. | John W. O'Leary, Bratin Saha, Mark R. Tuttle |
| 2008 | PODC | Extracting models from design documents with mapster. | David James, Tim Leonard, John W. O'Leary, Murali Talupur, Mark R. Tuttle |
| 2008 | PODC | Model checking transactional memory with spin. | John W. O'Leary, Bratin Saha, Mark R. Tuttle |
| 2007 | FMCAD | Verifying Correctness of Transactional Memories. | Ariel Cohen, John W. O'Leary, Amir Pnueli, Mark R. Tuttle, Lenore D. Zuck |
| 2000 | FMCAD | A Methodology for Large-Scale Hardware Verification. | Mark D. Aagaard, Robert B. Jones, Thomas F. Melham, John W. O'Leary, Carl-Johan H. Seger |
| 1996 | FMCAD | 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 |
| 1995 | ICCD | Verification of a subtractive radix-2 square root algorithm and implementation. | Miriam Leeser, John W. O'Leary |
| 1971 | WSC | Integrated circuit shop simulation for capacity planning and scheduling. | Dennis D. Newhart, John W. O'Leary |