The SCEAS System
Navigation Menu

Search the dblp DataBase

Title:
Author:

Warren A. Hunt Jr.: [Publications] [Author Rank by year] [Co-authors] [Prefers] [Cites] [Cited by]

Publications of Author

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

  29. Centaur Technology Media Unit Verification. [Citation Graph (, )][DBLP]


  30. Mechanized Information Flow Analysis through Inductive Assertions. [Citation Graph (, )][DBLP]


  31. Connecting pre-silicon and post-silicon verification. [Citation Graph (, )][DBLP]


  32. Mechanized Certification of Secure Hardware Designs. [Citation Graph (, )][DBLP]


  33. A Mechanically Verified AIG-to-BDD Conversion Algorithm. [Citation Graph (, )][DBLP]


Search in 0.385secs, Finished in 0.386secs
NOTICE1
System may not be available sometimes or not working properly, since it is still in development with continuous upgrades
NOTICE2
The rankings that are presented on this page should NOT be considered as formal since the citation info is incomplete in DBLP
 
System created by asidirop@csd.auth.gr [http://users.auth.gr/~asidirop/] © 2002
for Data Engineering Laboratory, Department of Informatics, Aristotle University © 2002