The paper presents an automatic iterative abstraction-refinement methodology for symbolic model checking, particularly for ACTL* specifications. The initial abstract model is generated by analyzing the control structures in the program to be verified. Abstract models may produce erroneous (or "spurious") counterexamples, which are analyzed and used to refine the abstract model. The refinement algorithm maintains a small abstract state space by using abstraction functions that distinguish multiple degrees of abstraction for each program variable. The methodology is implemented in NuSMV and validated through practical experiments, including a large Fujitsu IP core design with about 500 latches and 10,000 lines of SMV code. The approach is shown to be effective and competitive, with the ability to handle complex industrial designs. The paper also discusses the advantages of the proposed technique over previous methods, including completeness for a significant fragment of ACTL*, efficiency in initial abstraction and refinement, and the ability to distinguish multiple degrees of abstraction.The paper presents an automatic iterative abstraction-refinement methodology for symbolic model checking, particularly for ACTL* specifications. The initial abstract model is generated by analyzing the control structures in the program to be verified. Abstract models may produce erroneous (or "spurious") counterexamples, which are analyzed and used to refine the abstract model. The refinement algorithm maintains a small abstract state space by using abstraction functions that distinguish multiple degrees of abstraction for each program variable. The methodology is implemented in NuSMV and validated through practical experiments, including a large Fujitsu IP core design with about 500 latches and 10,000 lines of SMV code. The approach is shown to be effective and competitive, with the ability to handle complex industrial designs. The paper also discusses the advantages of the proposed technique over previous methods, including completeness for a significant fragment of ACTL*, efficiency in initial abstraction and refinement, and the ability to distinguish multiple degrees of abstraction.