For recent publications, please contact Jun Sawada .

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)