Mark Aagaard

2007
36	EE	Eunsuk Kang, Mark Aagaard: Improving the Usability of HOL Through Controlled Automation Tactics. TPHOLs 2007: 157-172
2005
35	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)
34	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
33	EE	Hazem I. Shehata, Mark Aagaard: A general decomposition strategy for verifying register renaming. DAC 2004: 234-237
32	EE	Mark Aagaard, Nancy A. Day, Robert B. Jones: Synchronization-at-Retirement for Pipeline Verification. FMCAD 2004: 113-127
31	EE	Mark Aagaard, Vlad C. Ciubotariu, Jason T. Higgins, Farzad Khalvati: Combining Equivalence Verification and Completion Functions. FMCAD 2004: 98-112
2003
30	EE	Mark Aagaard: A Hazards-Based Correctness Statement for Pipelined Circuits. CHARME 2003: 66-80
29	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
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	EE	Mark Aagaard, Nancy A. Day, Meng Lou: Relating Multi-step and Single-Step Microprocessor Correctness Statements. FMCAD 2002: 123-141
2001
26	EE	Robert Beers, Rajnish Ghughal, Mark Aagaard: Applications of Hierarchical Verification in Model Checking. CHARME 2001: 40-57
25	EE	Mark Aagaard, Byron Cook, Nancy A. Day, Robert B. Jones: A Framework for Microprocessor Correctness Statements. CHARME 2001: 433-448
24	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
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	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
21	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
20	EE	Robert Beers, Rajnish Ghughal, Mark Aagaard: Applications of Hierarchical Verification in Model Checking. FMCAD 2000
19	EE	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	EE	Mark Aagaard, Thomas F. Melham, John W. O'Leary: Xs are for Trajectory Evaluation, Booleans are for Theorem Proving. CHARME 1999: 202-218
16	EE	Mark Aagaard, Robert B. Jones, Carl-Johan H. Seger: Parametric Representations of Boolean Constraints. DAC 1999: 402-407
15	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
14	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
13	EE	Mark Aagaard, Carl-Johan H. Seger: The formal verification of a pipelined double-precision IEEE floating-point multiplier. ICCAD 1995: 7-10
12	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
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	EE	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	EE	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

Coauthor Index

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

Colors in the list of coauthors