Current Trends in Hardware Verification and Automated Theorem Proving

This report describes the partially completed correctness proof of the Viper ''block model''. Viper [7,8,9,11,23] is a microprocessor designed by W. J. Cullyer, C. Pygott and J. Kershaw at the Royal Signals and Radar Establishment in Malvern, England, (henceforth ''RSRE'') for use in safety-critical applications such as civil aviation and nuclear power plant control. It is currently finding uses i...