default search action
Mark D. Aagaard
Person information
- affiliation: University of Waterloo, Department of Electrical and Computer Engineering, ON, Canada
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2020 – today
- 2024
- [j18]Nusa Zidaric
, Kalikinkar Mandal, Guang Gong, Mark D. Aagaard:
The welch-gong stream cipher - evolutionary path. Cryptogr. Commun. 16(1): 129-165 (2024) - 2023
- [j17]Nusa Zidaric
FFCSA - Finite Field Constructions, Search, and Algorithms. ACM Commun. Comput. Algebra 57(2): 57-64 (2023) - [c35]Nusa Zidaric
Tower field support for synthesis of datapaths. CF 2023: 217-218 - 2021
- [i5]Mark D. Aagaard, Nusa Zidaric:
ASIC Benchmarking of Round 2 Candidates in the NIST Lightweight Cryptography Standardization Process: (Preliminary Results). IACR Cryptol. ePrint Arch. 2021: 49 (2021) - 2020
- [j16]Kalikinkar Mandal
Analysis and Efficient Implementations of a Class of Composited de Bruijn Sequences. IEEE Trans. Computers 69(12): 1835-1848 (2020) - [c34]Ahmed A. Ayoub, Mark D. Aagaard:
Application-Specific Instruction Set Architecture for an Ultralight Hardware Security Module. HOST 2020: 69-79
2010 – 2019
- 2019
- [j15]Nusa Zidaric
Hardware Optimizations and Analysis for the WG-16 Cipher with Tower Field Arithmetic. IEEE Trans. Computers 68(1): 67-82 (2019) - [i4]Mark D. Aagaard, Marat Sattarov, Nusa Zidaric:
Hardware Design and Analysis of the ACE and WAGE Ciphers. CoRR abs/1909.12338 (2019) - 2018
- [j14]Kalikinkar Mandal, Bo Yang, Guang Gong, Mark D. Aagaard:
On ideal t-tuple distribution of filtering de Bruijn sequence generators. Cryptogr. Commun. 10(4): 629-641 (2018) - [c33]Nusa Zidaric
Rapid Hardware Design for Cryptographic Modules with Filtering Structures over Small Finite Fields. WAIFI 2018: 128-145 - 2017
- [j13]Bo Yang, Kalikinkar Mandal, Mark D. Aagaard, Guang Gong:
Efficient Composited de Bruijn Sequence Generators. IEEE Trans. Computers 66(8): 1354-1368 (2017) - 2015
- [j12]Farzad Khalvati, Mark D. Aagaard, Hamid R. Tizhoosh:
Window memoization: toward high-performance image processing software. J. Real Time Image Process. 10(1): 5-25 (2015) - [c32]Gangqiang Yang, Bo Zhu, Valentin Suder, Mark D. Aagaard, Guang Gong:
The Simeck Family of Lightweight Block Ciphers. CHES 2015: 307-329 - [i3]Gangqiang Yang, Bo Zhu, Valentin Suder, Mark D. Aagaard, Guang Gong:
The Simeck Family of Lightweight Block Ciphers. IACR Cryptol. ePrint Arch. 2015: 612 (2015) - [i2]Gangqiang Yang, Mark D. Aagaard, Guang Gong:
Efficient Hardware Implementations of the Warbler Pseudorandom Number Generator. IACR Cryptol. ePrint Arch. 2015: 789 (2015) - 2014
- [j11]Kalikinkar Mandal, Guang Gong, Xinxin Fan, Mark D. Aagaard:
Optimal parameters for the WG stream cipher family. Cryptogr. Commun. 6(2): 117-135 (2014) - 2013
- [j10]Guang Gong, Mark D. Aagaard, Xinxin Fan:
Resilience to distinguishing attacks on WG-7 cipher and their generalizations. Cryptogr. Commun. 5(4): 277-289 (2013) - [c31]Gangqiang Yang, Xinxin Fan, Mark D. Aagaard, Guang Gong:
Design space exploration of the lightweight stream cipher WG-8 for FPGAs and ASICs. WESS 2013: 8:1-8:10 - [c30]Xinxin Fan, Nusa Zidaric
Efficient hardware implementation of the stream cipher WG-16 with composite field arithmetic. TrustED@CCS 2013: 21-34 - [c29]Kalikinkar Mandal, Guang Gong, Xinxin Fan, Mark D. Aagaard:
On selection of optimal parameters for the WG stream cipher family. CWIT 2013: 17-21 - [c28]Mark D. Aagaard, Guang Gong, Rajesh K. Mota:
Hardware implementations of the WG-5 cipher for passive RFID tags. HOST 2013: 29-34 - 2012
- [i1]Guang Gong, Mark D. Aagaard, Xinxin Fan:
Resilience to Distinguishing Attacks on WG-7 Cipher and Their Generalizations. IACR Cryptol. ePrint Arch. 2012: 681 (2012) - 2010
- [j9]Farzad Khalvati, Mark D. Aagaard:
Window memoization: an efficient hardware architecture for high-performance image processing. J. Real Time Image Process. 5(3): 195-212 (2010)
2000 – 2009
- 2007
- [c27]Eunsuk Kang, Mark D. Aagaard:
Improving the Usability of HOL Through Controlled Automation Tactics. TPHOLs 2007: 157-172 - 2005
- [j8]Carl-Johan H. Seger, Robert B. Jones, John W. O'Leary, Thomas F. Melham, Mark D. Aagaard, Clark W. Barrett
An industrially effective environment for formal hardware verification. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 24(9): 1381-1405 (2005) - [j7]Jason T. Higgins, Mark D. Aagaard:
Simplifying the design and automating the verification of pipelines with structural hazards. ACM Trans. Design Autom. Electr. Syst. 10(4): 651-672 (2005) - 2004
- [c26]Hazem I. Shehata
A general decomposition strategy for verifying register renaming. DAC 2004: 234-237 - [c25]Mark D. Aagaard, Vlad C. Ciubotariu, Jason T. Higgins, Farzad Khalvati:
Combining Equivalence Verification and Completion Functions. FMCAD 2004: 98-112 - [c24]Mark D. Aagaard, Nancy A. Day, Robert B. Jones:
Synchronization-at-Retirement for Pipeline Verification. FMCAD 2004: 113-127 - [c23]Jason T. Higgins, Mark D. Aagaard:
Simplifying design and verification for structural hazards and datapaths in pipelined circuits. HLDVT 2004: 31-36 - 2003
- [j6]Mark D. Aagaard, Byron Cook, Nancy A. Day, Robert B. Jones:
A framework for superscalar microprocessor correctness statements. Int. J. Softw. Tools Technol. Transf. 4(3): 298-312 (2003) - [c22]Mark D. Aagaard:
A Hazards-Based Correctness Statement for Pipelined Circuits. CHARME 2003: 66-80 - 2002
- [c21]Mark D. Aagaard, Nancy A. Day, Meng Lou:
Relating Multi-step and Single-Step Microprocessor Correctness Statements. FMCAD 2002: 123-141 - [e2]Mark D. Aagaard, John W. O'Leary:
Formal Methods in Computer-Aided Design, 4th International Conference, FMCAD 2002, Portland, OR, USA, November 6-8, 2002, Proceedings. Lecture Notes in Computer Science 2517, Springer 2002, ISBN 3-540-00116-6 [contents] - 2001
- [j5]Robert B. Jones, John W. O'Leary, Carl-Johan H. Seger, Mark D. Aagaard, Thomas F. Melham:
Practical Formal Verification in Microprocessor Design. IEEE Des. Test Comput. 18(4): 16-25 (2001) - [c20]Robert Beers, Rajnish Ghughal, Mark D. Aagaard:
Applications of Hierarchical Verification in Model Checking. CHARME 2001: 40-57 - [c19]Mark D. Aagaard, Byron Cook, Nancy A. Day, Robert B. Jones:
A Framework for Microprocessor Correctness Statements. CHARME 2001: 433-448 - 2000
- [c18]Mark D. Aagaard, Robert B. Jones, Roope Kaivola, Katherine R. Kohatsu, Carl-Johan H. Seger:
Formal verification of iterative algorithms in microprocessors. DAC 2000: 201-206 - [c17]Nancy A. Day, Mark D. Aagaard, Byron Cook:
Combining Stream-Based and State-Based Verification Techniques. FMCAD 2000: 126-142 - [c16]Mark D. Aagaard, Robert B. Jones, Thomas F. Melham, John W. O'Leary, Carl-Johan H. Seger:
A Methodology for Large-Scale Hardware Verification. FMCAD 2000: 263-282 - [c15]Robert Beers, Rajnish Ghughal, Mark D. Aagaard:
Applications of Hierarchical Verification in Model Checking. FMCAD 2000 - [c14]Roope Kaivola, Mark D. Aagaard:
Divider Circuit Verification with Model Checking and Theorem Proving. TPHOLs 2000: 338-355 - [e1]Mark D. Aagaard, John Harrison:
Theorem Proving in Higher Order Logics, 13th International Conference, TPHOLs 2000, Portland, Oregon, USA, August 14-18, 2000, Proceedings. Lecture Notes in Computer Science 1869, Springer 2000, ISBN 3-540-67863-8 [contents]
1990 – 1999
- 1999
- [c13]Mark D. Aagaard, Thomas F. Melham, John W. O'Leary:
Xs are for Trajectory Evaluation, Booleans are for Theorem Proving. CHARME 1999: 202-218 - [c12]Mark D. Aagaard, Robert B. Jones, Carl-Johan H. Seger:
Parametric Representations of Boolean Constraints. DAC 1999: 402-407 - [c11]Mark D. Aagaard, Robert B. Jones, Carl-Johan H. Seger:
Lifted-FL: A Pragmatic Implementation of Combined Model Checking and Theorem Proving. TPHOLs 1999: 323-340 - 1998
- [c10]Mark D. Aagaard, Robert B. Jones, Carl-Johan H. Seger:
Combining Theorem Proving and Trajectory Evaluation in an Industrial Environment. DAC 1998: 538-541 - 1995
- [j4]Mark D. Aagaard, Miriam Leeser
Verifying a Logic-Synthesis Algorithm and Implementation: A Case Study in Software Verification. IEEE Trans. Software Eng. 21(10): 822-833 (1995) - [c9]Mark D. Aagaard, Carl-Johan H. Seger:
The formal verification of a pipelined double-precision IEEE floating-point multiplier. ICCAD 1995: 7-10 - 1994
- [j3]Mark D. Aagaard, Miriam Leeser
A Methodology for Efficient Hardware Verification. Formal Methods Syst. Des. 5(1/2): 95-117 (1994) - [j2]Mark D. Aagaard, Miriam Leeser
PBS: proven Boolean simplification. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 13(4): 459-470 (1994) - [c8]Mark D. Aagaard, Miriam Leeser
Reasoning About Pipelines with Structural Hazards. TPCD 1994: 13-32 - [c7]John W. O'Leary, Miriam Leeser
Non-Restoring Integer Square Root: A Case Study in Design by Principled Optimization. TPCD 1994: 52-71 - 1993
- [j1]Miriam Leeser
High level synthesis and generating FPGAs with the BEDROC system. J. VLSI Signal Process. 6(2): 191-214 (1993) - [c6]John W. O'Leary, Mark H. Linderman, Miriam Leeser, Mark D. Aagaard:
HML: A Hardware Description Language Based on Standard ML. CHDL 1993: 327-334 - [c5]Mark D. Aagaard, Miriam Leeser:
A Framework for Specifying and Designing Pipelines. ICCD 1993: 548-551 - [c4]Mark D. Aagaard, Miriam Leeser, Phillip J. Windley:
Toward a Super Duper Hardware Tactic. HUG 1993: 399-412 - 1992
- [c3]Mark D. Aagaard, Miriam Leeser:
Verifying a Logic Synthesis Tool in Nuprl: A Case Study in Software Verification. CAV 1992: 69-81 - [c2]Mark D. Aagaard, Miriam Leeser:
A Methodology for Reusable Hardware Proofs. TPHOLs 1992: 177-196 - 1991
- [c1]Mark D. Aagaard, Miriam Leeser:
A Formally Verified System for Logic Synthesis. ICCD 1991: 346-350
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from ,
, and
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and
to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-05-08 21:04 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: