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
- Connectivity and internet of things
- Wireless communications and networks
- Application security
- Information security
- Infrastructure integrity
- Network Security
- Connectivity and Internet of Things
- Application domains
- Dependability and security
- 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
- Taught in 2019, 2020
- ECE 627 - Register-transfer-level Digital Systems
- Taught in 2020
* Only courses taught in the past 5 years are displayed.
- 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
- Yang, Gangqiang and Aagaard, Mark D and Gong, Guang, Efficient Hardware Implementations of the Warbler Pseudorandom Number Generator, , 2015
- 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
- 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
- Aagaard, Mark and Leeser, Miriam, A methodology for reusable hardware proofs, Proceedings of the IFIP TC10/WG10, 2, 2014, 177 - 196
- Currently considering applications from graduate students. A completed online application is required for admission; start the application process now.