Mark D. Aagaard, Robert B. Jones & Carl-Johan H. Seger (1999):
Formal verification using parametric representations of Boolean constraints.
In: DAC '99.
IEEE,
pp. 402–407,
doi:10.1145/309847.309968.
Sean Eron Anderson:
Bit Twiddling Hacks.
http://graphics.stanford.edu/ seander/bithacks.html.
Accessed June, 2011.
Michaël Armand, Germain Faure, Benjamin Grégoire, Chantal Keller, Laurent Théry & Benjamin Werner (2011):
Verifying SAT and SMT in Coq for a fully automated decision procedure.
In: PSATTT '11.
Robert S. Boyer & Warren A. Hunt, Jr. (2006):
Function Memoization and Unique Object Representation for ACL2 Functions.
In: ACL2 '06.
ACM,
pp. 81–89,
doi:10.1145/1217975.1217992.
Robert S. Boyer & Warren A. Hunt, Jr. (2009):
Symbolic Simulation in ACL2.
In: ACL2 '09.
ACM,
pp. 20–24,
doi:10.1145/1637837.1637840.
Yirng-An Chen & Randal E. Bryant (1998):
Verification of floating-point adders.
In: CAV '98,
LNCS 1427.
Springer,
pp. 488–499,
doi:10.1007/BFb0028769.
Ashish Darbari, Bernd Fischer & Jo"707Eao Marques-Silva (2010):
Industrial-Strength Certified SAT Solving through Verified SAT Proof Checking.
In: ICTAC '10,
LNCS 6255.
Springer,
pp. 260–274,
doi:10.1007/978-3-642-14808-8_18.
Jared Davis (2006):
Reasoning about File Input in ACL2.
In: ACL2 '06.
ACM,
pp. 117–126,
doi:10.1145/1217975.1218000.
Anthony Fox (2011):
LCF-Style Bit-Blasting in HOL4.
In: ITP '11,
LNCS.
Springer,
pp. 357–362,
doi:10.1007/978-3-642-22863-6_26.
Warren A. Hunt, Jr. & Sol Swords (2009):
Centaur Technology Media Unit Verification.
In: CAV '09,
LNCS 5643.
Springer,
pp. 353–367,
doi:10.1007/978-3-642-02658-4_28.
Warren A. Hunt, Jr., Sol Swords, Jared Davis & Anna Slobodová (2010):
Use of Formal Verification at Centaur Technology.
In: David Hardin: Design and Verification of Microprocessor Systems for High-Assurance Applications.
Springer,
pp. 65–88.
Matt Kaufmann, Panagiotis Manolios & J Strother Moore (2000):
Computer-Aided Reasoning: An Approach.
Kluwer Academic Publishers.
Panagiotis Manolios & Sudarshan K. Srinivasan (2006):
A Framework for Verifying Bit-Level Pipelined Machines Based on Automated Deduction and Decision Procedures.
Journal of Automated Reasoning 37(1-2),
pp. 93–116,
doi:10.1007/s10817-006-9035-0.
John McCarthy (1960):
Recursive Functions of Symbolic Expressions and Their Computation by Machine, Part 1.
Communications of the ACM 3(4),
pp. 184–195,
doi:10.1145/367177.367199.
Erik Reeber & Warren A. Hunt, Jr. (2006):
A SAT-Based Decision Procedure for the Subclass of Unrollable List Functions in ACL2 (SULFA)..
In: IJCAR '06,
LNCS 4130.
Springer,
pp. 453–467,
doi:10.1007/11814771_38.
Erik Henry Reeber (2007):
Combining Advanced Formal Hardware Verification Techniques.
University of Texas at Austin.
http://hdl.handle.net/2152/3662.
Anna Slobodová, Jared Davis, Sol Swords & Warren A. Hunt, Jr. (2011):
A Flexible Formal Verification Framework for Industrial Scale Validation.
In: Memocode '11.
IEEE,
pp. 89–97,
doi:10.1109/MEMCOD.2011.5970515.
Sundarshan Kumar Srinivasan (2007):
Efficient Verification of Bit-Level Pipelined Machines Using Refinement.
Georgia Institute of Technology.
http://hdl.handle.net/1853/19815.
Sol Swords & Warren A. Hunt, Jr. (2010):
A Mechanically Verified AIG to BDD Conversion Algorithm.
In: ITP '10,
LNCS 6172.
Springer,
pp. 435–449,
doi:10.1007/978-3-642-14052-5_30.
Sol Otis Swords (2010):
A Verified Framework for Symbolic Execution in the ACL2 Theorem Prover.
University of Texas at Austin.
http://hdl.handle.net/2152/ETD-UT-2010-12-2210.
Tjark Weber & Hasan Amjad (2009):
Efficiently Checking Propositional Refutations in HOL Theorem Provers.
Journal of Applied Logic 7(1),
pp. 26–40,
doi:10.1016/j.jal.2007.07.003.
eptcs@eptcs.org