Bibliography
 
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): 298-312, 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 micro-architecture. 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 computer-aided design 1996.
  • Z. Manna, A. Pnueli Temporal Verification of Reactive Systems, Safety. Springer-Verlag, 1995 (p.104-152)
 
Top-level Refinement in Processor Verification
  •   S.Krstic, B.Cook, J.Launchbury, J.Matthews, "Top-level Refinement in Processor Verification", 1998
  •   J.Burch, D.Dill , "Automatic verification of pipelined microprocessor control", 1994
 
Verification of Out-Of-Order Processor Designs Using Completion Function with Reference File
  •   S. Berezin, E. Clarke, A. Biere, Y. Zhu, "Verification of Out-Of-Order Processor Designs Using Model Checking and a Light-Weight Completion Function", 2002
  •   S. Berezin, A. Biere, E. Clarke, andY. Zhu, .Combining symbolic model checking with uninterpreted functions for out-of-order processor verification,. 1998
 
Specification and Verification of HDL models (2 themes)
  •   David M. Russinoff, Specification and Verification of Gate-Level 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.Sangiovanni-Vincentelli "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 38-52.