Abstract: This paper presents a method for using abstraction to reduce the complexity of temporal logic model checking. The method involves constructing an abstract model of a program without examining the unabstracted model. The abstract model is used to verify properties of the original program. The authors implemented a system based on these techniques and demonstrated their practicality using examples, including a pipelined ALU circuit with over 10^1300 states. The paper discusses the use of Boolean decision diagrams (BDDs) to represent transition relations and the development of abstractions for reasoning about programs. The authors propose several useful abstractions, including congruence modulo an integer, single bit abstractions, product abstractions, and symbolic abstractions. They demonstrate the practicality of their methods by considering examples such as a 16-bit by 16-bit hardware multiplier and a pipelined ALU circuit. The paper also discusses the relationship between abstraction and model checking, showing that abstraction can be used to verify properties of programs with large state spaces. The authors conclude that their approach is conservative in certain cases and exact in others, depending on the properties being verified.Abstract: This paper presents a method for using abstraction to reduce the complexity of temporal logic model checking. The method involves constructing an abstract model of a program without examining the unabstracted model. The abstract model is used to verify properties of the original program. The authors implemented a system based on these techniques and demonstrated their practicality using examples, including a pipelined ALU circuit with over 10^1300 states. The paper discusses the use of Boolean decision diagrams (BDDs) to represent transition relations and the development of abstractions for reasoning about programs. The authors propose several useful abstractions, including congruence modulo an integer, single bit abstractions, product abstractions, and symbolic abstractions. They demonstrate the practicality of their methods by considering examples such as a 16-bit by 16-bit hardware multiplier and a pipelined ALU circuit. The paper also discusses the relationship between abstraction and model checking, showing that abstraction can be used to verify properties of programs with large state spaces. The authors conclude that their approach is conservative in certain cases and exact in others, depending on the properties being verified.