Note: I am slowly adding links to copies of these papers. If I haven't yet added the one of interest to you, please send me email.
Mark D. Aagaard and John W. O'Leary, editors, Formal Methods in Computer-Aided Design, volume 2517 of LNCS, Springer; New York, 2002.
Mark D. Aagaard and John R. Harrison, editors, Theorem Proving in Higher Order Logics, volume 1869 of LNCS, Springer; New York, 2000.
Mark D. Aagaard, Byron Cook, Nancy A. Day, and Robert B. Jones A Framework for Superscalar Microprocessor Correctness Statements, International Journal on Software Tools for Technology Transfer, Springer Verlag, online publication: Dec 17, 2002.
Robert B. Jones, John W. O'Leary, Carl-Johan H. Seger, Mark D. Aagaard, and Thomas F. Melham. Practical Formal Verification in Microprocessor Design . IEEE Design and Test, 18(4): 1625, November 2001.
Mark D. Aagaard and Miriam E. Leeser Verifying a Logic-Synthesis Algorithm and Implementation: A Case Study in Software Verification . IEEE Transactions on Software Engineering, Volume 21, Number 10, October 1995, pp 822-833
Mark D. Aagaard and Miriam E. Leeser A Methodology for Efficient Hardware Verification Formal Methods in Systems Design vol 5 (1 & 2), 95-117, July, 1994.
Mark D. Aagaard and Miriam E. Leeser. Proven Boolean Simplification IEEE Transactions on Computer-Aided Design, Vol. 13, No. 4, pp. 459-470, April, 1994.
Miriam Leeser, Richard Chapman, Mark Aagaard, Mark Linderman, and Stephan Meier. High level synthesis and generating FPGAs with the BEDROC system. Journal of VLSI Signal Processing, 6(2):193--216, August 1993.
Mark D. Aagaard, Nancy A. Day, and Meng Lou, Relating Multi-step and Single-step Microprocessor Correctness Statements, in Formal Methods in Computer-Aided Design (FMCAD). LNCS, Volume 2517, Springer Verlag; New York, November, 2002, pp. 123-141.
Mark D. Aagaard, Byron Cook, Nancy A. Day, and Robert B. Jones A Framework for Microprocessor Correctness Statements, CHARME 2001, LNCS, Volume 2144, Livingston, Scotland, Sept 4-7, 2001.
Nancy A. Day, Mark D. Aagaard, and Byron Cook. Combining stream-based and state-based verification techniques for microarchitectures. In Warren Hunt and Steve Johnson, editors, Formal Methods in Computer-Aided Design (FMCAD). LNCS, Volume 1954, Springer Verlag; New York, November 2000.
Mark D. Aagaard, Robert B. Jones, John W. O'Leary, Carl-Johan H. Seger, and Thomas F Melham. A methodology for large-scale hardware verification. In Warren Hunt and Steve Johnson, editors, Formal Methods in Computer-Aided Design (FMCAD). LNCS, Volume 1954, Springer Verlag; New York, November 2000.
Robert H. Beers, Rajnish Ghughal, and Mark D. Aagaard. Applications of hierarchical verification in model checking. In Warren Hunt and Steve Johnson, editors, Formal Methods in Computer-Aided Design (FMCAD). Springer Verlag; New York, November 2000 (appears in CHARME 2001 proceedings).
Roope Kaivola and Mark D. Aagaard. Divider circuit verification with model checking and theorem proving. In Mark D. Aagaard and John R. Harrison, editors, Theorem Proving in Higher Order Logics (TPHOLs), pages 338--355. Springer Verlag; New York, August 2000.
Mark D. Aagaard, Robert B. Jones, Katherine R Kohatsu, Roope Kaivola, and Carl-Johan H. Seger. Formal verification of iterative algorithms in microprocessors. In ACM/IEEE Design Automation Conference (DAC), June 2000.
Mark D. Aagaard, Thomas F. Melham, and John W. O'Leary, Xs are for Trajectory Evaluation, Booleans are for Theorem Proving Correct Hardware Design and Verification Methods (CHARME), 1999.
Mark D. Aagaard, Robert B. Jones, Carl-Johan H. Seger, Lifted-FL: A Pragmatic Implementation of Combined Model Checking and Theorem Proving Theorem Proving in Higher Order Logics (TPHOLs), LNCS, Volume 1690, Springer Verlag, 1999.
Mark D. Aagaard, Robert B. Jones, Carl-Johan H. Seger, Formal Verification Using Parametric Representations of Boolean Constraints, Design Automation Conference (DAC), 1999.
Mark D. Aagaard, Robert B. Jones, Carl-Johan H. Seger, Combining Theorem Proving and Trajectory Evaluation in an Industrial Environment, Design Automation Conference (DAC), 538-541, 1998.
Mark D. Aagaard Carl-Johan H. Seger The Formal Verification of a Pipelined Double-Precision IEEE Floating-Point Multiplier International Conference on Computer Aided Design (ICCAD), 7-10, 1995.
John W. O'Leary, Miriam E. Leeser, Jason Hickey, and Mark D. Aagaard. Non-Restoring Integer Square Root: A Case Study in Design by Principled Optimization. International Conference on Theorem Provers in Circuit Design (TPCD), October, 1994. Published in vol. 901 of Lecture Notes in Computer Science, (T. Kropf and R. Kumar, eds.), pp. 52-71, Springer Verlag, 1995.
Mark D. Aagaard and Miriam E. Leeser Reasoning about Pipelines with Structural Hazards International Conference on Theorem Provers in Circuit Design (TPCD), 1994.
Mark D. Aagaard, Miriam E. Leeser and Phillip J. Windley Towards a Super Duper Hardware Tactic HOL User's Group Meeting, 1993, Springer-Verlag.
Mark D. Aagaard and Miriam E. Leeser Verifying a Logic Synthesis Tool in Nuprl: A Case Study in Software Verification Computer Aided Verification (CAV), 69-81, 1993.
Mark D. Aagaard and Miriam E. Leeser A Methodology for Efficient Hardware Verification HOL User's Group Meeting, pp177-196, 1992.
Mark D. Aagaard and Miriam E. Leeser A Formally Verified System for Logic Synthesis International Conference on Computers and Computer Design (ICCD), 1991.
Nancy A. Day, Mark D. Aagaard, and Meng Lou, A Formal Analysis of the Will-Retire Correctness Statement, Technical Report 2002-14, Department of Computer Science, March, 2002.
Nancy A. Day, Mark D. Aagaard, and Meng Lou, A Mechanized Theory for Microprocessor Correctness Statements, Technical Report 2002-11, Department of Computer Science, March, 2002.
Mark D. Aagaard, Thomas F. Melham, and John W. O'Leary, Xs are for Trajectory Evaluation, Booleans are for Theorem Proving University of Glasgow, 1999.
Mark D. Aagaard and Miriam E. Leeser A Theorem Proving Based Methodology for Software Verification Technical Report 93-1335, Department of Computer Science, Cornell University, March,1993.
Mark Aagaard and Miriam Leeser A Framework for Specifying and Designing Pipelines Technical Report EE-CEG-93-3, School of Electrical Engineering , Cornell University, April, 1993.
Mark Aagaard and Miriam Leeser PBS: Proven Boolean Simplification Technical Report EE-CEG-92-4, Cornell University, School of Electrical Engineering, June, 1992.