Abstract :
The design of the Viper microprocessor represents a major advance in the use of mathematics to formally verify the correctness of a logic design. Viper is likely to become an important element in many safety-critical computer systems, and will have an extensive influence on hardware technology
