Mark Aagaard

2007
35	EE	Eunsuk Kang, Mark Aagaard: Improving the Usability of HOL Through Controlled Automation Tactics. TPHOLs 2007: 157-172
2005
34	EE	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)
33	EE	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
32	EE	Hazem I. Shehata, Mark Aagaard: A general decomposition strategy for verifying register renaming. DAC 2004: 234-237
31	EE	Mark Aagaard, Nancy A. Day, Robert B. Jones: Synchronization-at-Retirement for Pipeline Verification. FMCAD 2004: 113-127
30	EE	Mark Aagaard, Vlad C. Ciubotariu, Jason T. Higgins, Farzad Khalvati: Combining Equivalence Verification and Completion Functions. FMCAD 2004: 98-112
2003
29	EE	Mark Aagaard: A Hazards-Based Correctness Statement for Pipelined Circuits. CHARME 2003: 66-80
28	EE	Mark Aagaard, Byron Cook, Nancy A. Day, Robert B. Jones: A framework for superscalar microprocessor correctness statements. STTT 4(3): 298-312 (2003)
2002
27		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
26	EE	Mark Aagaard, Nancy A. Day, Meng Lou: Relating Multi-step and Single-Step Microprocessor Correctness Statements. FMCAD 2002: 123-141
2001
25	EE	Robert Beers, Rajnish Ghughal, Mark Aagaard: Applications of Hierarchical Verification in Model Checking. CHARME 2001: 40-57
24	EE	Mark Aagaard, Byron Cook, Nancy A. Day, Robert B. Jones: A Framework for Microprocessor Correctness Statements. CHARME 2001: 433-448
23	EE	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
22		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
21	EE	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
20	EE	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
19	EE	Robert Beers, Rajnish Ghughal, Mark Aagaard: Applications of Hierarchical Verification in Model Checking. FMCAD 2000
18	EE	Nancy A. Day, Mark Aagaard, Byron Cook: Combining Stream-Based and State-Based Verification Techniques. FMCAD 2000: 126-142
17		Roope Kaivola, Mark Aagaard: Divider Circuit Verification with Model Checking and Theorem Proving. TPHOLs 2000: 338-355
1999
16	EE	Mark Aagaard, Thomas F. Melham, John W. O'Leary: Xs are for Trajectory Evaluation, Booleans are for Theorem Proving. CHARME 1999: 202-218
15	EE	Mark Aagaard, Robert B. Jones, Carl-Johan H. Seger: Parametric Representations of Boolean Constraints. DAC 1999: 402-407
14	EE	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
13	EE	Mark Aagaard, Robert B. Jones, Carl-Johan H. Seger: Combining Theorem Proving and Trajectory Evaluation in an Industrial Environment. DAC 1998: 538-541
1995
12	EE	Mark Aagaard, Carl-Johan H. Seger: The formal verification of a pipelined double-precision IEEE floating-point multiplier. ICCAD 1995: 7-10
11	EE	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
10		Mark Aagaard, Miriam Leeser: Reasoning About Pipelines with Structural Hazards. TPCD 1994: 13-32
9		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
8		Mark Aagaard, Miriam Leeser: A Methodology for Efficient Hardware Verification. Formal Methods in System Design 5(1/2): 95-117 (1994)
7	EE	Mark Aagaard, Miriam Leeser: PBS: proven Boolean simplification. IEEE Trans. on CAD of Integrated Circuits and Systems 13(4): 459-470 (1994)
1993
6		John W. O'Leary, Mark H. Linderman, Miriam Leeser, Mark Aagaard: HML: A Hardware Description Language Based on Standard ML. CHDL 1993: 327-334
5		Mark Aagaard, Miriam Leeser, Phillip J. Windley: Toward a Super Duper Hardware Tactic. HUG 1993: 399-412
4		Mark Aagaard, Miriam Leeser: A Framework for Specifying and Designing Pipelines. ICCD 1993: 548-551
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

Coauthor Index

1	Clark Barrett	[33]
2	Robert Beers	[19] [25]
3	Vlad C. Ciubotariu	[30]
4	Byron Cook	[18] [24] [28]
5	Nancy A. Day	[18] [24] [26] [28] [31]
6	Rajnish Ghughal	[19] [25]
7	John Harrison	[22]
8	Jason Hickey	[9]
9	Jason T. Higgins	[30] [34]
10	Robert B. Jones	[13] [14] [15] [20] [21] [23] [24] [28] [31] [33]
11	Roope Kaivola	[17] [21]
12	Eunsuk Kang	[35]
13	Farzad Khalvati	[30]
14	Katherine R. Kohatsu	[21]
15	Miriam Leeser	[1] [2] [3] [4] [5] [6] [7] [8] [9] [10] [11]
16	Mark H. Linderman	[6]
17	Meng Lou	[26]
18	Thomas F. Melham	[16] [20] [23] [33]
19	John W. O'Leary	[6] [9] [16] [20] [23] [27] [33]
20	Carl-Johan H. Seger	[12] [13] [14] [15] [20] [21] [23] [33]
21	Hazem I. Shehata	[32]
22	Don Syme	[33]
23	Phillip J. Windley	[5]

Colors in the list of coauthors