Author of the publication

Linear and Nonlinear Arithmetic in ACL2.

, , and . CHARME, volume 2860 of Lecture Notes in Computer Science, page 319-333. Springer, (2003)

Please choose a person to relate this publication to

To differ between persons with the same name, the academic degree and the title of an important publication will be displayed. You can also use the button next to the name to display some publications already assigned to the person.

 

Other publications of authors with the same name

Verifying the FM9801 microarchitecture., and . IEEE Micro, 19 (3): 47-55 (1999)A SAT-based procedure for verifying finite state machines in ACL2., and . ACL2, page 127-135. ACM, (2006)Processor Verification with Precise Exeptions and Speculative Execution., and . CAV, volume 1427 of Lecture Notes in Computer Science, page 135-146. Springer, (1998)The Verification of a Bit-slice ALU., and . Hardware Specification, Verification and Synthesis, volume 408 of Lecture Notes in Computer Science, page 282-306. Springer, (1989)Results of the Verification of a Complex Pipelined Machine Model., and . CHARME, volume 1703 of Lecture Notes in Computer Science, page 313-316. Springer, (1999)Verification of FM9801: An Out-of-Order Microprocessor Model with Speculative Execution, Exceptions, and Program-Modifying Capability., and . Formal Methods Syst. Des., 20 (2): 187-222 (2002)Automatic insertion of low power annotations in RTL for pipelined microprocessors., , and . DATE, page 496-501. European Design and Automation Association, Leuven, Belgium, (2006)A Mechanically Verified AIG-to-BDD Conversion Algorithm., and . ITP, volume 6172 of Lecture Notes in Computer Science, page 435-449. Springer, (2010)Trimming while checking clausal proofs., , and . FMCAD, page 181-188. IEEE, (2013)Toward Verified Execution Environments., , and . S&P, page 106-115. IEEE Computer Society, (1987)