

Algebraic Models of Correctness for Microprocessors 
 A.C.J. Fox and N.A. Harman, Algebraic Models of Correctness for Microprocessors. Formal Aspects of Computing, 12(4): 298312, 2000.
 A.C.J. Fox An Algebraic Models for Advanced Microprocessors., PhD thesis, University of Wales Swansea, 1998.


Specification and Verification of Microprocessor in HOL 
 A.C.J. Fox An Algebraic Framework for Modelling and Verifying Microprocessors Using HOL., 2001.
 A.C.J. Fox, A HOL Specification of the ARM Instruction Set Architecture. Technical report No. 545, University of Cambridge Computer Laboratory, June 2001.
 A.C.J. Fox, Formal verification of the ARM6 microarchitecture. Technical report No. 548, University of Cambridge Computer Laboratory, November 2002.


Automatic Generation of Invariants in Processor Verification 
 Jeffrey X. Su, David L. Dill, Clark W. Barrett, Automatic Generation of Invariants in Processor Verification. First international conference on formal methods in computeraided design 1996.
 Z. Manna, A. Pnueli Temporal Verification of Reactive Systems, Safety. SpringerVerlag, 1995 (p.104152)


Toplevel Refinement in Processor Verification 
 S.Krstic, B.Cook, J.Launchbury, J.Matthews, "Toplevel Refinement in Processor Verification", 1998
 J.Burch, D.Dill , "Automatic verification of pipelined microprocessor
control", 1994


Verification of OutOfOrder Processor Designs Using Completion Function with Reference File 
 S. Berezin, E. Clarke, A. Biere, Y. Zhu, "Verification of OutOfOrder Processor Designs Using Model Checking and a LightWeight Completion Function", 2002
 S. Berezin, A. Biere, E. Clarke, andY. Zhu, .Combining symbolic model checking with uninterpreted functions for outoforder processor verification,. 1998


Specification and Verification of HDL models (2 themes) 
 David M. Russinoff, Specification and Verification of GateLevel VHDL Models of Synchronous and Asynchronous Circuits. 1994


Hardware Verification using Monadic Second Order Logic 
 David A. Basin, Nils Klarrund, Hardware Verification using Monadic Second Order Logic. 1995
 A. Aziz, F.Balarin, K.Brayton, A.SangiovanniVincentelli "Sequential Synthesis Using S1S", 2000


Verification of Synchronous Circuits by Symbolic Logic Simulation (Proseminar) 
 R.E.Bryant, "Verification of Synchronous Circuits by Symbolic Logic Simulation", 1989.


Relative Timing Based Verification of Timed Circuits and Systems (Proseminar) 
 H.Kim, P.A.Beerel, K.Stevens "Relative Timing Based Verification of Timed
Circuits and Systems", 2001


Formal Specification of Abstract Memory Models (Proseminar) 
 David L. Dill and Seungjoon Park and Andreas G. Nowatzyk, "Formal Specification of Abstract Memory Models," Proceedings of the 1993 Symposium, Gaetano Borriello and Carl Ebeling, Eds. MIT Press, 1993, pp 3852.

