Mechanically checking a lemma used in an automatic verification tool

This publication has 15 references indexed in Scilit:

• The Stanford FLASH multiprocessor
  Published by Institute of Electrical and Electronics Engineers (IEEE) ,2002
• Applying formal verification to a commercial microprocessor
  Published by Institute of Electrical and Electronics Engineers (IEEE) ,2002
• Efficient validity checking for processor verification
  Published by Institute of Electrical and Electronics Engineers (IEEE) ,2002
• Applying formal verification to the AAMP5 microprocessor: A case study in the industrial use of formal methods
  Formal Methods in System Design, 1996
• Techniques for verifying superscalar microprocessors
  Published by Association for Computing Machinery (ACM) ,1996
• Automatic verification of pipelined microprocessor control
  Published by Springer Nature ,1994
• Formal verification of a pipelined microprocessor
  IEEE Software, 1990
• HOL: A Proof Generating System for Higher-Order Logic
  Published by Springer Nature ,1988
• A Proof of Correctness of the Viper Microprocessor: The First Level
  Published by Springer Nature ,1988
• A formulation of the simple theory of types
  The Journal of Symbolic Logic, 1940