Warren A. Hunt Jr.

2008
33	EE	Sandip Ray, Warren A. Hunt Jr., John Matthews, J. Strother Moore: A Mechanical Analysis of Program Verification Strategies. J. Autom. Reasoning 40(4): 245-269 (2008)
2007
32	EE	Sandip Ray, Warren A. Hunt Jr.: Mechanized Certification of Secure Hardware Designs. MTV 2007: 25-32
2006
31	EE	Warren A. Hunt Jr., Erik Reeber: A SAT-based procedure for verifying finite state machines in ACL2. ACL2 2006: 127-135
30	EE	Michael J. C. Gordon, Warren A. Hunt Jr., Matt Kaufmann, James Reynolds: An embedding of the ACL2 logic in HOL. ACL2 2006: 40-46
29	EE	Robert S. Boyer, Warren A. Hunt Jr.: Function memoization and unique object representation for ACL2 functions. ACL2 2006: 81-89
28	EE	Warren A. Hunt Jr., Serita M. Nelesen: Phylogenetic trees in ACL2. ACL2 2006: 99-102
27	EE	Vinod Viswanath, Jacob A. Abraham, Warren A. Hunt Jr.: Automatic insertion of low power annotations in RTL for pipelined microprocessors. DATE 2006: 496-501
26	EE	Michael J. C. Gordon, James Reynolds, Warren A. Hunt Jr., Matt Kaufmann: An Integration of HOL and ACL2. FMCAD 2006: 153-160
25	EE	Erik Reeber, Warren A. Hunt Jr.: A SAT-Based Decision Procedure for the Subclass of Unrollable List Formulas in ACL2 (SULFA). IJCAR 2006: 453-467
2005
24	EE	Warren A. Hunt Jr., Erik Reeber: Formalization of the DE2 Language. CHARME 2005: 20-34
23	EE	Warren A. Hunt Jr., Matt Kaufmann, Robert Bellarmine Krug, J. Strother Moore, Eric Whitman Smith: Meta Reasoning in ACL2. TPHOLs 2005: 163-178
22	EE	Robert S. Boyer, Warren A. Hunt Jr., Serita M. Nelesen: A Compressed Format for Collections of Phylogenetic Trees and Improved Consensus Performance. WABI 2005: 353-364
2004
21	EE	Sandip Ray, Warren A. Hunt Jr.: Deductive Verification of Pipelined Machines Using First-Order Quantification. CAV 2004: 31-43
20	EE	Warren A. Hunt Jr.: Mechanical Mathematical Methods for Microprocessor Verification. CAV 2004: 523-533
2003
19		Warren A. Hunt Jr., Fabio Somenzi: Computer Aided Verification, 15th International Conference, CAV 2003, Boulder, CO, USA, July 8-12, 2003, Proceedings Springer 2003
18	EE	Warren A. Hunt Jr., Robert Bellarmine Krug, J. Strother Moore: Linear and Nonlinear Arithmetic in ACL2. CHARME 2003: 319-333
17	EE	William Adams, Warren A. Hunt Jr., Damir Jamsek: Verisym: Verifying Circuits by Symbolic Simulation. Formal Methods in System Design 22(2): 163-173 (2003)
16	EE	Ganesh Gopalakrishnan, Warren A. Hunt Jr.: Industrial Practice of Formal Hardware Verification: A Sampling. Formal Methods in System Design 22(2): 95-99 (2003)
2002
15		Warren A. Hunt Jr.: Introduction: Special Issue on Microprocessor Verifications. Formal Methods in System Design 20(2): 135-137 (2002)
14		Jun Sawada, Warren A. Hunt Jr.: Verification of FM9801: An Out-of-Order Microprocessor Model with Speculative Execution, Exceptions, and Program-Modifying Capability. Formal Methods in System Design 20(2): 187-222 (2002)
2000
13		Warren A. Hunt Jr., Steven D. Johnson: Formal Methods in Computer-Aided Design, Third International Conference, FMCAD 2000, Austin, Texas, USA, November 1-3, 2000, Proceedings Springer 2000
12	EE	Jun Sawada, Warren A. Hunt Jr.: Hardware Modeling Using Function Encapsulation. FMCAD 2000: 234-245
1999
11	EE	Jun Sawada, Warren A. Hunt Jr.: Results of the Verification of a Complex Pipelined Machine Model. CHARME 1999: 313-316
1998
10		Jun Sawada, Warren A. Hunt Jr.: Processor Verification with Precise Exeptions and Speculative Execution. CAV 1998: 135-146
1997
9		Jun Sawada, Warren A. Hunt Jr.: Trace Table Based Approach for Pipeline Microprocessor Verification. CAV 1997: 364-375
8		Bishop Brock, Warren A. Hunt Jr.: Formally Specifying and Mechanically Verifying Programs for the Motorola Complex Arithmetic Processor DSP. ICCD 1997: 31-36
7		Bishop Brock, Warren A. Hunt Jr.: The DUAL-EVAL Hardware Description Language and Its Use in the Formal Specification and Verification of the FM9001 Microprocessor. Formal Methods in System Design 11(1): 71-104 (1997)
1994
6		Warren A. Hunt Jr.: FM8501: A Verified Microprocessor Springer 1994
1992
5		Bishop Brock, Warren A. Hunt Jr., William D. Young: Introduction to a Formally Defined Hardware Description Language. TPCD 1992: 3-35
1989
4		Warren A. Hunt Jr., Bishop Brock: The Verification of a Bit-slice ALU. Hardware Specification, Verification and Synthesis 1989: 282-306
3		William R. Bevier, Warren A. Hunt Jr., J. Strother Moore, William D. Young: An Approach to Systems Verification. J. Autom. Reasoning 5(4): 411-428 (1989)
2		Warren A. Hunt Jr.: Microprocessor Design Verification. J. Autom. Reasoning 5(4): 429-460 (1989)
1987
1		William R. Bevier, Warren A. Hunt Jr., William D. Young: Toward Verified Execution Environments. IEEE Symposium on Security and Privacy 1987: 106-115

Coauthor Index

1	Jacob A. Abraham	[27]
2	William Adams	[17]
3	William R. Bevier	[1] [3]
4	Robert S. Boyer	[22] [29]
5	Bishop Brock	[4] [5] [7] [8]
6	Ganesh Gopalakrishnan	[16]
7	Michael J. C. Gordon	[26] [30]
8	Damir Jamsek	[17]
9	Steven D. Johnson	[13]
10	Matt Kaufmann	[23] [26] [30]
11	Robert Bellarmine Krug	[18] [23]
12	John Matthews	[33]
13	J. Strother Moore	[3] [18] [23] [33]
14	Serita M. Nelesen	[22] [28]
15	Sandip Ray	[21] [32] [33]
16	Erik Reeber	[24] [25] [31]
17	James Reynolds	[26] [30]
18	Jun Sawada	[9] [10] [11] [12] [14]
19	Eric Whitman Smith	[23]
20	Fabio Somenzi	[19]
21	Vinod Viswanath	[27]
22	William D. Young	[1] [3] [5]

Colors in the list of coauthors