 | 2010 |
| 37 |  | Farzad Khalvati,
Mark Aagaard:
Window memoization: an efficient hardware architecture for high-performance image processing.
J. Real-Time Image Processing 5(3): 195-212 (2010) |
| 2007 |
| 36 |  | Eunsuk Kang,
Mark Aagaard:
Improving the Usability of HOL Through Controlled Automation Tactics.
TPHOLs 2007: 157-172 |
| 2005 |
| 35 |  | Jason T. Higgins,
Mark Aagaard:
Simplifying the design and automating the verification of pipelines with structural hazards.
ACM Trans. Design Autom. Electr. Syst. 10(4): 651-672 (2005) |
| 34 |  | Carl-Johan H. Seger,
Robert B. Jones,
John W. O'Leary,
Thomas F. Melham,
Mark Aagaard,
Clark Barrett,
Don Syme:
An industrially effective environment for formal hardware verification.
IEEE Trans. on CAD of Integrated Circuits and Systems 24(9): 1381-1405 (2005) |
| 2004 |
| 33 |  | Hazem I. Shehata,
Mark Aagaard:
A general decomposition strategy for verifying register renaming.
DAC 2004: 234-237 |
| 32 |  | Mark Aagaard,
Nancy A. Day,
Robert B. Jones:
Synchronization-at-Retirement for Pipeline Verification.
FMCAD 2004: 113-127 |
| 31 |  | Mark Aagaard,
Vlad C. Ciubotariu,
Jason T. Higgins,
Farzad Khalvati:
Combining Equivalence Verification and Completion Functions.
FMCAD 2004: 98-112 |
| 2003 |
| 30 |  | Mark Aagaard:
A Hazards-Based Correctness Statement for Pipelined Circuits.
CHARME 2003: 66-80 |
| 29 |  | Mark Aagaard,
Byron Cook,
Nancy A. Day,
Robert B. Jones:
A framework for superscalar microprocessor correctness statements.
STTT 4(3): 298-312 (2003) |
| 2002 |
| 28 |  | Mark Aagaard,
John W. O'Leary:
Formal Methods in Computer-Aided Design, 4th International Conference, FMCAD 2002, Portland, OR, USA, November 6-8, 2002, Proceedings
Springer 2002 |
| 27 |  | Mark Aagaard,
Nancy A. Day,
Meng Lou:
Relating Multi-step and Single-Step Microprocessor Correctness Statements.
FMCAD 2002: 123-141 |
| 2001 |
| 26 |  | Robert Beers,
Rajnish Ghughal,
Mark Aagaard:
Applications of Hierarchical Verification in Model Checking.
CHARME 2001: 40-57 |
| 25 |  | Mark Aagaard,
Byron Cook,
Nancy A. Day,
Robert B. Jones:
A Framework for Microprocessor Correctness Statements.
CHARME 2001: 433-448 |
| 24 |  | Robert B. Jones,
John W. O'Leary,
Carl-Johan H. Seger,
Mark Aagaard,
Thomas F. Melham:
Practical Formal Verification in Microprocessor Design.
IEEE Design & Test of Computers 18(4): 16-25 (2001) |
| 2000 |
| 23 |  | Mark Aagaard,
John Harrison:
Theorem Proving in Higher Order Logics, 13th International Conference, TPHOLs 2000, Portland, Oregon, USA, August 14-18, 2000, Proceedings
Springer 2000 |
| 22 |  | Mark Aagaard,
Robert B. Jones,
Roope Kaivola,
Katherine R. Kohatsu,
Carl-Johan H. Seger:
Formal verification of iterative algorithms in microprocessors.
DAC 2000: 201-206 |
| 21 |  | Mark 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 |
| 20 |  | Robert Beers,
Rajnish Ghughal,
Mark Aagaard:
Applications of Hierarchical Verification in Model Checking.
FMCAD 2000 |
| 19 |  | Nancy A. Day,
Mark Aagaard,
Byron Cook:
Combining Stream-Based and State-Based Verification Techniques.
FMCAD 2000: 126-142 |
| 18 |  | Roope Kaivola,
Mark Aagaard:
Divider Circuit Verification with Model Checking and Theorem Proving.
TPHOLs 2000: 338-355 |
| 1999 |
| 17 |  | Mark Aagaard,
Thomas F. Melham,
John W. O'Leary:
Xs are for Trajectory Evaluation, Booleans are for Theorem Proving.
CHARME 1999: 202-218 |
| 16 |  | Mark Aagaard,
Robert B. Jones,
Carl-Johan H. Seger:
Parametric Representations of Boolean Constraints.
DAC 1999: 402-407 |
| 15 |  | Mark 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 |
| 14 |  | Mark Aagaard,
Robert B. Jones,
Carl-Johan H. Seger:
Combining Theorem Proving and Trajectory Evaluation in an Industrial Environment.
DAC 1998: 538-541 |
| 1995 |
| 13 |  | Mark Aagaard,
Carl-Johan H. Seger:
The formal verification of a pipelined double-precision IEEE floating-point multiplier.
ICCAD 1995: 7-10 |
| 12 |  | Mark 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) |
| 1994 |
| 11 |  | Mark Aagaard,
Miriam Leeser:
Reasoning About Pipelines with Structural Hazards.
TPCD 1994: 13-32 |
| 10 |  | John W. O'Leary,
Miriam Leeser,
Jason Hickey,
Mark Aagaard:
Non-Restoring Integer Square Root: A Case Study in Design by Principled Optimization.
TPCD 1994: 52-71 |
| 9 |  | Mark Aagaard,
Miriam Leeser:
A Methodology for Efficient Hardware Verification.
Formal Methods in System Design 5(1/2): 95-117 (1994) |
| 8 |  | Mark Aagaard,
Miriam Leeser:
PBS: proven Boolean simplification.
IEEE Trans. on CAD of Integrated Circuits and Systems 13(4): 459-470 (1994) |
| 1993 |
| 7 |  | John W. O'Leary,
Mark H. Linderman,
Miriam Leeser,
Mark Aagaard:
HML: A Hardware Description Language Based on Standard ML.
CHDL 1993: 327-334 |
| 6 |  | Mark Aagaard,
Miriam Leeser,
Phillip J. Windley:
Toward a Super Duper Hardware Tactic.
HUG 1993: 399-412 |
| 5 |  | Mark Aagaard,
Miriam Leeser:
A Framework for Specifying and Designing Pipelines.
ICCD 1993: 548-551 |
| 4 |  | Miriam Leeser,
Richard Chapman,
Mark Aagaard,
Mark H. Linderman,
Stephan Meier:
High level synthesis and generating FPGAs with the BEDROC system.
VLSI Signal Processing 6(2): 191-214 (1993) |
| 1992 |
| 3 |  | Mark Aagaard,
Miriam Leeser:
Verifying a Logic Synthesis Tool in Nuprl: A Case Study in Software Verification.
CAV 1992: 69-81 |
| 2 |  | Mark Aagaard,
Miriam Leeser:
A Methodology for Reusable Hardware Proofs.
TPHOLs 1992: 177-196 |
| 1991 |
| 1 |  | Mark Aagaard,
Miriam Leeser:
A Formally Verified System for Logic Synthesis.
ICCD 1991: 346-350 |