| 2018 | WAIFI | Rapid Hardware Design for Cryptographic Modules with Filtering Structures over Small Finite Fields. | Nusa Zidaric, Mark D. Aagaard, Guang Gong |
| 2015 | CHES | The Simeck Family of Lightweight Block Ciphers. | Gangqiang Yang, Bo Zhu, Valentin Suder, Mark D. Aagaard, Guang Gong |
| 2013 | CASES | Design space exploration of the lightweight stream cipher WG-8 for FPGAs and ASICs. | Gangqiang Yang, Xinxin Fan, Mark D. Aagaard, Guang Gong |
| 2013 | CCS | Efficient hardware implementation of the stream cipher WG-16 with composite field arithmetic. | Xinxin Fan, Nusa Zidaric, Mark D. Aagaard, Guang Gong |
| 2004 | DAC | A general decomposition strategy for verifying register renaming. | Hazem I. Shehata, Mark D. Aagaard |
| 2004 | FMCAD | Combining Equivalence Verification and Completion Functions. | Mark D. Aagaard, Vlad C. Ciubotariu, Jason T. Higgins, Farzad Khalvati |
| 2004 | FMCAD | Synchronization-at-Retirement for Pipeline Verification. | Mark D. Aagaard, Nancy A. Day, Robert B. Jones |
| 2002 | FMCAD | Relating Multi-step and Single-Step Microprocessor Correctness Statements. | Mark D. Aagaard, Nancy A. Day, Meng Lou |
| 2000 | DAC | Formal verification of iterative algorithms in microprocessors. | Mark D. Aagaard, Robert B. Jones, Roope Kaivola, Katherine R. Kohatsu, Carl-Johan H. Seger |
| 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 |
| 2000 | FMCAD | Applications of Hierarchical Verification in Model Checking. | Robert Beers, Rajnish Ghughal, Mark D. Aagaard |
| 2000 | FMCAD | Combining Stream-Based and State-Based Verification Techniques. | Nancy A. Day, Mark D. Aagaard, Byron Cook |
| 1999 | DAC | Parametric Representations of Boolean Constraints. | Mark D. Aagaard, Robert B. Jones, Carl-Johan H. Seger |
| 1998 | DAC | Combining Theorem Proving and Trajectory Evaluation in an Industrial Environment. | Mark D. Aagaard, Robert B. Jones, Carl-Johan H. Seger |
| 1995 | ICCAD | The formal verification of a pipelined double-precision IEEE floating-point multiplier. | Mark D. Aagaard, Carl-Johan H. Seger |
| 1993 | ICCD | A Framework for Specifying and Designing Pipelines. | Mark D. Aagaard, Miriam Leeser |
| 1992 | CAV | Verifying a Logic Synthesis Tool in Nuprl: A Case Study in Software Verification. | Mark D. Aagaard, Miriam Leeser |
| 1991 | ICCD | A Formally Verified System for Logic Synthesis. | Mark D. Aagaard, Miriam Leeser |