dblp.uni-trier.dewww.uni-trier.de

Warren A. Hunt Jr. Vis

List of publications from the DBLP Bibliography Server - FAQ
Coauthor Index - Ask others: ACM DL/Guide - CiteSeerX - CSB - MetaPress - Google - Bing - Yahoo
Home Page

*2009
35EEWarren A. Hunt Jr., Sol Swords: Centaur Technology Media Unit Verification. CAV 2009: 353-367
2008
34EEWarren A. Hunt Jr., Robert Bellarmine Krug, Sandip Ray, William D. Young: Mechanized Information Flow Analysis through Inductive Assertions. FMCAD 2008: 1-4
33EESandip 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
32EESandip Ray, Warren A. Hunt Jr.: Mechanized Certification of Secure Hardware Designs. MTV 2007: 25-32
2006
31EEWarren A. Hunt Jr., Erik Reeber: A SAT-based procedure for verifying finite state machines in ACL2. ACL2 2006: 127-135
30EEMichael J. C. Gordon, Warren A. Hunt Jr., Matt Kaufmann, James Reynolds: An embedding of the ACL2 logic in HOL. ACL2 2006: 40-46
29EERobert S. Boyer, Warren A. Hunt Jr.: Function memoization and unique object representation for ACL2 functions. ACL2 2006: 81-89
28EEWarren A. Hunt Jr., Serita M. Nelesen: Phylogenetic trees in ACL2. ACL2 2006: 99-102
27EEVinod Viswanath, Jacob A. Abraham, Warren A. Hunt Jr.: Automatic insertion of low power annotations in RTL for pipelined microprocessors. DATE 2006: 496-501
26EEMichael J. C. Gordon, James Reynolds, Warren A. Hunt Jr., Matt Kaufmann: An Integration of HOL and ACL2. FMCAD 2006: 153-160
25EEErik 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
24EEWarren A. Hunt Jr., Erik Reeber: Formalization of the DE2 Language. CHARME 2005: 20-34
23EEWarren A. Hunt Jr., Matt Kaufmann, Robert Bellarmine Krug, J. Strother Moore, Eric Whitman Smith: Meta Reasoning in ACL2. TPHOLs 2005: 163-178
22EERobert 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
21EESandip Ray, Warren A. Hunt Jr.: Deductive Verification of Pipelined Machines Using First-Order Quantification. CAV 2004: 31-43
20EEWarren 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
18EEWarren A. Hunt Jr., Robert Bellarmine Krug, J. Strother Moore: Linear and Nonlinear Arithmetic in ACL2. CHARME 2003: 319-333
17EEWilliam Adams, Warren A. Hunt Jr., Damir Jamsek: Verisym: Verifying Circuits by Symbolic Simulation. Formal Methods in System Design 22(2): 163-173 (2003)
16EEGanesh 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
12EEJun Sawada, Warren A. Hunt Jr.: Hardware Modeling Using Function Encapsulation. FMCAD 2000: 234-245
1999
11EEJun Sawada, Warren A. Hunt Jr.: Results of the Verification of a Complex Pipelined Machine Model. CHARME 1999: 313-316
1998
10EEJun Sawada, Warren A. Hunt Jr.: Processor Verification with Precise Exeptions and Speculative Execution. CAV 1998: 135-146
1997
9EEJun 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
4EEWarren 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

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

Colors in the list of coauthors

Copyright © Tue Nov 3 08:52:44 2009 by Michael Ley (ley@uni-trier.de)