Mark Aagaard is an Associate Professor in the Department of Electrical and Computer Engineering at the University of Waterloo.
His research interests include formal methods for the design and verification of digital-hardware systems. He has developed a formal theory for pipelined circuits that is based on the conventional ideas of structural hazards, control hazards, data hazards and datapath functionality. Professor Aagaard’s current research activities use different formalization aspects of pipeline hazards to explore new design and verification techniques for varying classes of hazards.
Some recent projects of Professor Aagaard’s include verifying data-hazard accuracy, exploiting the power and usability of an off-the-shelf combinational equivalence checker, and developing a prototype design and verification tool that includes a cell library of control components for pipeline stages. Professor Aagaard also took part in creating the Microbox framework for microprocessor correctness statements, where over 30 published verification results were analyzed and proved correctness statement conditions.
- Formal Verification
- Design And Verification Of Digital Hardware System
- Computer Architecture
- Computer & Software Engineering
- 1994, Doctorate, Electrical Engineering, Cornell University
- 1991, Master of Science, Electrical Engineering, Cornell University
- 1988, Bachelor of Science (BS), Electrical Engineering, Harvey Mudd College
- ECE 327 - Digital Hardware Systems
- ECE 627 - Register-transfer-level Digital Systems
- Yang, Gangqiang and Aagaard, Mark D and Gong, Guang, Efficient Hardware Implementations of the Warbler Pseudorandom Number Generator, , 2015
- Khalvati, Farzad and Aagaard, Mark D and Tizhoosh, Hamid R, Window memoization: toward high-performance image processing software, Journal of Real-Time Image Processing, 10(1), 2015, 5 - 25
- Aagaard, Mark and Leeser, Miriam, A methodology for reusable hardware proofs, Proceedings of the IFIP TC10/WG10, 2, 2014, 177 - 196
- O'Leary, John and Linderman, Mark and Leeser, Miriam and Aagaard, Mark, HML: A Hardware Description Language, Computer Hardware Description Languages and their Applications: Proceedings of the 11th IFIP WG10. 2 International Conference on Computer Hardware Description Languages and their Applications-CHDL'93 Sponsored by IFIP WG10. 2 and in cooperation with , 32, 2014
- Mandal, Kalikinkar and Gong, Guang and Fan, Xinxin and Aagaard, Mark, Optimal parameters for the WG stream cipher family, Cryptography and Communications, 6(2), 2014, 117 - 135
- Gong, Guang and Aagaard, Mark and Fan, Xinxin, Resilience to distinguishing attacks on WG-7 cipher and their generalizations, Cryptography and Communications, 5(4), 2013, 277 - 289
- Yang, Gangqiang and Zhu, Bo and Suder, Valentin and Aagaard, Mark D and Gong, Guang, The simeck family of lightweight block ciphers, International Workshop on Cryptographic Hardware and Embedded Systems, January 2015, 307 - 329
- Mandal, Kalikinkar and Gong, Guang and Fan, Xinxin and Aagaard, Mark, On selection of optimal parameters for the WG stream cipher family, Information Theory (CWIT), 2013 13th Canadian Workshop on, January 2013, 17 - 21
- Yang, Gangqiang and Fan, Xinxin and Aagaard, Mark and Gong, Guang, Design space exploration of the lightweight stream cipher WG-8 for FPGAs and ASICs, Proceedings of the Workshop on Embedded Systems Security, January 2013
- Fan, Xinxin and Zidaric, Nusa and Aagaard, Mark and Gong, Guang, Efficient hardware implementation of the stream cipher WG-16 with composite field arithmetic, Proceedings of the 3rd international workshop on Trustworthy embedded devices, January 2013, 21 - 34
- Aagaard, Mark D and Gong, Guang and Mota, Rajesh K, Hardware implementations of the WG-5 cipher for passive RFID tags, Hardware-Oriented Security and Trust (HOST), 2013 IEEE International Symposium on, January 2013, 29 - 34
- Gong, Guang and Aagaard, Mark David and Xinxin, FAN, Lightweight stream cipher cryptosystems, January