Publications during the Graduate Study at the
University of Texas
Formal Verification of an Advanced Microprocessor Model (Ph.D Thesis) (web
page) (pub info)
Verification of a Simple Pipelined Machine Model. (in ACL2 book) (ps)
(pub info)
Verifying the FM9801 Microarchitecture (in IEEE Micro 99) (pdf)
(pub info)
Results of the Verification of a Complex Pipelined Machine Model. (in CHARME
99) (ps) (pub
info)
Processor Verification with Precise Exceptions and Speculative Execution.
(in CAV 98) (ps) (pub
info)
Trace Table Based Approach for Pipelined Microprocessor Verification. (in
CAV 97) (ps) (pub info)
Dissertation Proposal Paper. (ps)
Formal Verification of Pipelined Machines with Out-of-order Execution.
(ps) (tech report attached to the dissertation
proposal).
Decomposing the Verification of Pipelined Microprocessors with Invariant
Conditions (unpublished) (ps)
Verification of a Pipelined Machine with Out-of-Order Instruction
Completion. (unpublished tech report) (ps)