Mark D. Aagaard

60 papers A* 5A 2B 7C 3Journal 23Unranked 19

Year	Rank	Type	Title / Venue / Authors
2024	J	`jnl`	The welch-gong stream cipher - evolutionary path. Cryptogr. Commun. Nusa Zidaric, Kalikinkar Mandal, Guang Gong, Mark D. Aagaard
2023	J	`jnl`	FFCSA - Finite Field Constructions, Search, and Algorithms. ACM Commun. Comput. Algebra Nusa Zidaric, Guang Gong, Mark D. Aagaard, Aleksandar Jurisic, Olexandr Konovalov
2023	—	`conf`	Tower field support for synthesis of datapaths. CF Nusa Zidaric, Mark D. Aagaard
2021	J	`jnl`	ASIC Benchmarking of Round 2 Candidates in the NIST Lightweight Cryptography Standardization Process: (Preliminary Results). IACR Cryptol. ePrint Arch. Mark D. Aagaard, Nusa Zidaric
2020	J	`jnl`	Analysis and Efficient Implementations of a Class of Composited de Bruijn Sequences. IEEE Trans. Computers Kalikinkar Mandal, Bo Yang, Guang Gong, Mark D. Aagaard
2020	—	`conf`	Application-Specific Instruction Set Architecture for an Ultralight Hardware Security Module. HOST Ahmed A. Ayoub, Mark D. Aagaard
2019	J	`jnl`	Hardware Design and Analysis of the ACE and WAGE Ciphers. CoRR Mark D. Aagaard, Marat Sattarov, Nusa Zidaric
2019	J	`jnl`	Hardware Optimizations and Analysis for the WG-16 Cipher with Tower Field Arithmetic. IEEE Trans. Computers Nusa Zidaric, Mark D. Aagaard, Guang Gong
2018	J	`jnl`	On ideal t-tuple distribution of filtering de Bruijn sequence generators. Cryptogr. Commun. Kalikinkar Mandal, Bo Yang, Guang Gong, Mark D. Aagaard
2018	C	`conf`	Rapid Hardware Design for Cryptographic Modules with Filtering Structures over Small Finite Fields. WAIFI Nusa Zidaric, Mark D. Aagaard, Guang Gong
2017	J	`jnl`	Efficient Composited de Bruijn Sequence Generators. IEEE Trans. Computers Bo Yang, Kalikinkar Mandal, Mark D. Aagaard, Guang Gong
2015	J	`jnl`	Efficient Hardware Implementations of the Warbler Pseudorandom Number Generator. IACR Cryptol. ePrint Arch. Gangqiang Yang, Mark D. Aagaard, Guang Gong
2015	A	`conf`	The Simeck Family of Lightweight Block Ciphers. CHES Gangqiang Yang, Bo Zhu, Valentin Suder, Mark D. Aagaard, Guang Gong
2015	J	`jnl`	The Simeck Family of Lightweight Block Ciphers. IACR Cryptol. ePrint Arch. Gangqiang Yang, Bo Zhu, Valentin Suder, Mark D. Aagaard, Guang Gong
2015	J	`jnl`	Window memoization: toward high-performance image processing software. J. Real Time Image Process. Farzad Khalvati, Mark D. Aagaard, Hamid R. Tizhoosh
2014	J	`jnl`	Optimal parameters for the WG stream cipher family. Cryptogr. Commun. Kalikinkar Mandal, Guang Gong, Xinxin Fan, Mark D. Aagaard
2013	—	`conf`	Design space exploration of the lightweight stream cipher WG-8 for FPGAs and ASICs. WESS Gangqiang Yang, Xinxin Fan, Mark D. Aagaard, Guang Gong
2013	—	`conf`	Efficient hardware implementation of the stream cipher WG-16 with composite field arithmetic. TrustED@CCS Xinxin Fan, Nusa Zidaric, Mark D. Aagaard, Guang Gong
2013	—	`conf`	Hardware implementations of the WG-5 cipher for passive RFID tags. HOST Mark D. Aagaard, Guang Gong, Rajesh K. Mota
2013	—	`conf`	On selection of optimal parameters for the WG stream cipher family. CWIT Kalikinkar Mandal, Guang Gong, Xinxin Fan, Mark D. Aagaard
2013	J	`jnl`	Resilience to distinguishing attacks on WG-7 cipher and their generalizations. Cryptogr. Commun. Guang Gong, Mark D. Aagaard, Xinxin Fan
2012	J	`jnl`	Resilience to Distinguishing Attacks on WG-7 Cipher and Their Generalizations. IACR Cryptol. ePrint Arch. Guang Gong, Mark D. Aagaard, Xinxin Fan
2010	J	`jnl`	Window memoization: an efficient hardware architecture for high-performance image processing. J. Real Time Image Process. Farzad Khalvati, Mark D. Aagaard
2007	—	`conf`	Improving the Usability of HOL Through Controlled Automation Tactics. TPHOLs Eunsuk Kang, Mark D. Aagaard
2005	J	`jnl`	An industrially effective environment for formal hardware verification. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. Carl-Johan H. Seger, Robert B. Jones, John W. O'Leary, Thomas F. Melham, Mark D. Aagaard, Clark W. Barrett, Don Syme
2005	J	`jnl`	Simplifying the design and automating the verification of pipelines with structural hazards. ACM Trans. Design Autom. Electr. Syst. Jason T. Higgins, Mark D. Aagaard
2004	A*	`conf`	A general decomposition strategy for verifying register renaming. DAC Hazem I. Shehata, Mark D. Aagaard
2004	B	`conf`	Combining Equivalence Verification and Completion Functions. FMCAD Mark D. Aagaard, Vlad C. Ciubotariu, Jason T. Higgins, Farzad Khalvati
2004	—	`conf`	Simplifying design and verification for structural hazards and datapaths in pipelined circuits. HLDVT Jason T. Higgins, Mark D. Aagaard
2004	B	`conf`	Synchronization-at-Retirement for Pipeline Verification. FMCAD Mark D. Aagaard, Nancy A. Day, Robert B. Jones
2003	—	`conf`	A Hazards-Based Correctness Statement for Pipelined Circuits. CHARME Mark D. Aagaard
2003	J	`jnl`	A framework for superscalar microprocessor correctness statements. Int. J. Softw. Tools Technol. Transf. Mark D. Aagaard, Byron Cook, Nancy A. Day, Robert B. Jones
2002	B	`ed.`	Formal Methods in Computer-Aided Design, 4th International Conference, FMCAD 2002, Portland, OR, USA, November 6-8, 2002, Proceedings FMCAD Mark D. Aagaard, John W. O'Leary
2002	B	`conf`	Relating Multi-step and Single-Step Microprocessor Correctness Statements. FMCAD Mark D. Aagaard, Nancy A. Day, Meng Lou
2001	—	`conf`	A Framework for Microprocessor Correctness Statements. CHARME Mark D. Aagaard, Byron Cook, Nancy A. Day, Robert B. Jones
2001	—	`conf`	Applications of Hierarchical Verification in Model Checking. CHARME Robert Beers, Rajnish Ghughal, Mark D. Aagaard
2001	J	`jnl`	Practical Formal Verification in Microprocessor Design. IEEE Des. Test Comput. Robert B. Jones, John W. O'Leary, Carl-Johan H. Seger, Mark D. Aagaard, Thomas F. Melham
2000	B	`conf`	A Methodology for Large-Scale Hardware Verification. FMCAD Mark D. Aagaard, Robert B. Jones, Thomas F. Melham, John W. O'Leary, Carl-Johan H. Seger
2000	B	`conf`	Applications of Hierarchical Verification in Model Checking. FMCAD Robert Beers, Rajnish Ghughal, Mark D. Aagaard
2000	B	`conf`	Combining Stream-Based and State-Based Verification Techniques. FMCAD Nancy A. Day, Mark D. Aagaard, Byron Cook
2000	—	`conf`	Divider Circuit Verification with Model Checking and Theorem Proving. TPHOLs Roope Kaivola, Mark D. Aagaard
2000	A*	`conf`	Formal verification of iterative algorithms in microprocessors. DAC Mark D. Aagaard, Robert B. Jones, Roope Kaivola, Katherine R. Kohatsu, Carl-Johan H. Seger
2000	—	`ed.`	Theorem Proving in Higher Order Logics, 13th International Conference, TPHOLs 2000, Portland, Oregon, USA, August 14-18, 2000, Proceedings TPHOLs Mark D. Aagaard, John Harrison
1999	—	`conf`	Lifted-FL: A Pragmatic Implementation of Combined Model Checking and Theorem Proving. TPHOLs Mark D. Aagaard, Robert B. Jones, Carl-Johan H. Seger
1999	A*	`conf`	Parametric Representations of Boolean Constraints. DAC Mark D. Aagaard, Robert B. Jones, Carl-Johan H. Seger
1999	—	`conf`	Xs are for Trajectory Evaluation, Booleans are for Theorem Proving. CHARME Mark D. Aagaard, Thomas F. Melham, John W. O'Leary
1998	A*	`conf`	Combining Theorem Proving and Trajectory Evaluation in an Industrial Environment. DAC Mark D. Aagaard, Robert B. Jones, Carl-Johan H. Seger
1995	A	`conf`	The formal verification of a pipelined double-precision IEEE floating-point multiplier. ICCAD Mark D. Aagaard, Carl-Johan H. Seger
1995	J	`jnl`	Verifying a Logic-Synthesis Algorithm and Implementation: A Case Study in Software Verification. IEEE Trans. Software Eng. Mark D. Aagaard, Miriam Leeser
1994	J	`jnl`	A Methodology for Efficient Hardware Verification. Formal Methods Syst. Des. Mark D. Aagaard, Miriam Leeser
1994	—	`conf`	Non-Restoring Integer Square Root: A Case Study in Design by Principled Optimization. TPCD John W. O'Leary, Miriam Leeser, Jason Hickey, Mark D. Aagaard
1994	J	`jnl`	PBS: proven Boolean simplification. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. Mark D. Aagaard, Miriam Leeser
1994	—	`conf`	Reasoning About Pipelines with Structural Hazards. TPCD Mark D. Aagaard, Miriam Leeser
1993	C	`conf`	A Framework for Specifying and Designing Pipelines. ICCD Mark D. Aagaard, Miriam Leeser
1993	—	`conf`	HML: A Hardware Description Language Based on Standard ML. CHDL John W. O'Leary, Mark H. Linderman, Miriam Leeser, Mark D. Aagaard
1993	J	`jnl`	High level synthesis and generating FPGAs with the BEDROC system. J. VLSI Signal Process. Miriam Leeser, Richard Chapman, Mark D. Aagaard, Mark H. Linderman, Stephan Meier
1993	—	`conf`	Toward a Super Duper Hardware Tactic. HUG Mark D. Aagaard, Miriam Leeser, Phillip J. Windley
1992	—	`conf`	A Methodology for Reusable Hardware Proofs. TPHOLs Mark D. Aagaard, Miriam Leeser
1992	A*	`conf`	Verifying a Logic Synthesis Tool in Nuprl: A Case Study in Software Verification. CAV Mark D. Aagaard, Miriam Leeser
1991	C	`conf`	A Formally Verified System for Logic Synthesis. ICCD Mark D. Aagaard, Miriam Leeser