We describe a method for using abstraction to reduce the complexity of
temporal-logic model checking. Using techniques similar to those invo
lved in abstract interpretation, we construct an abstract model of a p
rogram without ever examining the corresponding unabstracted model. We
show how this abstract model can be used to verify properties of the
original program. We have implemented a system based on these techniqu
es, and we demonstrate their practicality using a number of examples,
including a program representing a pipelined ALU circuit with over 10(
1300) states.