A Formally Verified System for Logic Synthesis. - Mark D. Aagaard; Miriam Leeser (ICCD, 1991)

Verifying a Logic Synthesis Tool in Nuprl: A Case Study in Software Verification. - Mark D. Aagaard; Miriam Leeser (CAV, 1992)

A Methodology for Reusable Hardware Proofs. - Mark D. Aagaard; Miriam Leeser (TPHOLs, 1992)

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

A Framework for Specifying and Designing Pipelines. - Mark D. Aagaard; Miriam Leeser (ICCD, 1993)

Toward a Super Duper Hardware Tactic. - Mark D. Aagaard; Miriam Leeser; Phillip J. Windley (HUG, 1993)

High level synthesis and generating FPGAs with the BEDROC system. - Miriam Leeser; Richard Chapman 001; Mark D. Aagaard; Mark H. Linderman; Stephan Meier (J. VLSI Signal Process., 1993)

Reasoning About Pipelines with Structural Hazards. - Mark D. Aagaard; Miriam Leeser (TPCD, 1994)

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)

A Methodology for Efficient Hardware Verification. - Mark D. Aagaard; Miriam Leeser (Formal Methods Syst. Des., 1994)

PBS: proven Boolean simplification. - Mark D. Aagaard; Miriam Leeser (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1994)

The formal verification of a pipelined double-precision IEEE floating-point multiplier. - Mark D. Aagaard; Carl-Johan H. Seger (ICCAD, 1995)

Verifying a Logic-Synthesis Algorithm and Implementation: A Case Study in Software Verification. - Mark D. Aagaard; Miriam Leeser (IEEE Trans. Software Eng., 1995)

Combining Theorem Proving and Trajectory Evaluation in an Industrial Environment. - Mark D. Aagaard; Robert B. Jones; Carl-Johan H. Seger (DAC, 1998)

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

Parametric Representations of Boolean Constraints. - Mark D. Aagaard; Robert B. Jones; Carl-Johan H. Seger (DAC, 1999)

Lifted-FL: A Pragmatic Implementation of Combined Model Checking and Theorem Proving. - Mark D. Aagaard; Robert B. Jones; Carl-Johan H. Seger (TPHOLs, 1999)

Formal verification of iterative algorithms in microprocessors. - Mark D. Aagaard; Robert B. Jones; Roope Kaivola; Katherine R. Kohatsu; Carl-Johan H. Seger (DAC, 2000)

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)

Combining Stream-Based and State-Based Verification Techniques. - Nancy A. Day; Mark D. Aagaard; Byron Cook (FMCAD, 2000)

Divider Circuit Verification with Model Checking and Theorem Proving. - Roope Kaivola; Mark D. Aagaard (TPHOLs, 2000)

A Framework for Microprocessor Correctness Statements. - Mark D. Aagaard; Byron Cook; Nancy A. Day; Robert B. Jones (CHARME, 2001)

Applications of Hierarchical Verification in Model Checking. - Robert Beers; Rajnish Ghughal; Mark D. Aagaard (CHARME, 2001)

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)

Relating Multi-step and Single-Step Microprocessor Correctness Statements. - Mark D. Aagaard; Nancy A. Day; Meng Lou (FMCAD, 2002)

A Hazards-Based Correctness Statement for Pipelined Circuits. - Mark D. Aagaard (CHARME, 2003)

A framework for superscalar microprocessor correctness statements. - Mark D. Aagaard; Byron Cook; Nancy A. Day; Robert B. Jones (Int. J. Softw. Tools Technol. Transf., 2003)

A general decomposition strategy for verifying register renaming. - Hazem I. Shehata; Mark D. Aagaard (DAC, 2004)

Combining Equivalence Verification and Completion Functions. - Mark D. Aagaard; Vlad C. Ciubotariu; Jason T. Higgins; Farzad Khalvati (FMCAD, 2004)

Synchronization-at-Retirement for Pipeline Verification. - Mark D. Aagaard; Nancy A. Day; Robert B. Jones (FMCAD, 2004)

Simplifying design and verification for structural hazards and datapaths in pipelined circuits. - Jason T. Higgins; Mark D. Aagaard (HLDVT, 2004)

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)

Simplifying the design and automating the verification of pipelines with structural hazards. - Jason T. Higgins; Mark D. Aagaard (ACM Trans. Design Autom. Electr. Syst., 2005)

Improving the Usability of HOL Through Controlled Automation Tactics. - Eunsuk Kang; Mark D. Aagaard (TPHOLs, 2007)

Window memoization: an efficient hardware architecture for high-performance image processing. - Farzad Khalvati; Mark D. Aagaard (J. Real Time Image Process., 2010)

Design space exploration of the lightweight stream cipher WG-8 for FPGAs and ASICs. - Gangqiang Yang; Xinxin Fan; Mark D. Aagaard; Guang Gong (WESS, 2013)

Efficient hardware implementation of the stream cipher WG-16 with composite field arithmetic. - Xinxin Fan; Nusa Zidaric; Mark D. Aagaard; Guang Gong (TrustED@CCS, 2013)

On selection of optimal parameters for the WG stream cipher family. - Kalikinkar Mandal; Guang Gong; Xinxin Fan; Mark D. Aagaard (CWIT, 2013)

Hardware implementations of the WG-5 cipher for passive RFID tags. - Mark D. Aagaard; Guang Gong; Rajesh K. Mota (HOST, 2013)

Resilience to distinguishing attacks on WG-7 cipher and their generalizations. - Guang Gong; Mark D. Aagaard; Xinxin Fan (Cryptogr. Commun., 2013)

Optimal parameters for the WG stream cipher family. - Kalikinkar Mandal; Guang Gong; Xinxin Fan; Mark D. Aagaard (Cryptogr. Commun., 2014)

Efficient Hardware Implementations of the Warbler Pseudorandom Number Generator. - Gangqiang Yang; Mark D. Aagaard; Guang Gong (IACR Cryptol. ePrint Arch., 2015)

The Simeck Family of Lightweight Block Ciphers. - Gangqiang Yang; Bo Zhu 007; Valentin Suder; Mark D. Aagaard; Guang Gong (IACR Cryptol. ePrint Arch., 2015)

Window memoization: toward high-performance image processing software. - Farzad Khalvati; Mark D. Aagaard; Hamid R. Tizhoosh (J. Real Time Image Process., 2015)

Efficient Composited de Bruijn Sequence Generators. - Bo Yang; Kalikinkar Mandal; Mark D. Aagaard; Guang Gong (IEEE Trans. Computers, 2017)

Rapid Hardware Design for Cryptographic Modules with Filtering Structures over Small Finite Fields. - Nusa Zidaric; Mark D. Aagaard; Guang Gong (WAIFI, 2018)

On ideal t-tuple distribution of filtering de Bruijn sequence generators. - Kalikinkar Mandal; Bo Yang; Guang Gong; Mark D. Aagaard (Cryptogr. Commun., 2018)

Hardware Design and Analysis of the ACE and WAGE Ciphers. - Mark D. Aagaard; Marat Sattarov; Nusa Zidaric (CoRR, 2019)

Hardware Optimizations and Analysis for the WG-16 Cipher with Tower Field Arithmetic. - Nusa Zidaric; Mark D. Aagaard; Guang Gong (IEEE Trans. Computers, 2019)

Application-Specific Instruction Set Architecture for an Ultralight Hardware Security Module. - Ahmed A. Ayoub; Mark D. Aagaard (HOST, 2020)

Analysis and Efficient Implementations of a Class of Composited de Bruijn Sequences. - Kalikinkar Mandal; Bo Yang; Guang Gong; Mark D. Aagaard (IEEE Trans. Computers, 2020)

ASIC Benchmarking of Round 2 Candidates in the NIST Lightweight Cryptography Standardization Process: (Preliminary Results). - Mark D. Aagaard; Nusa Zidaric (IACR Cryptol. ePrint Arch., 2021)

Tower field support for synthesis of datapaths. - Nusa Zidaric; Mark D. Aagaard (CF, 2023)

FFCSA - Finite Field Constructions, Search, and Algorithms. - Nusa Zidaric; Guang Gong; Mark D. Aagaard; Aleksandar Jurisic; Olexandr Konovalov (ACM Commun. Comput. Algebra, 2023)

The welch-gong stream cipher - evolutionary path. - Nusa Zidaric; Kalikinkar Mandal; Guang Gong; Mark D. Aagaard (Cryptogr. Commun., 2024)