A new heuristic for bad cycle detection using BDDs

  • R. H. Hardin
  • R. P. Kurshan
  • S. K. Shukla
  • M. Y. Vardi
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1254)


We describe a new heuristic for detecting bad cycles (reachable cycles that are not confined within one or another designated sets of model states), a fundamental operation for model-checking algorithms. It is a variation on a standard implementation of the Emerson-Lei algorithm, which our experimental data suggests can result in a significant speed-up for verification runs that pass. We conclude that this heuristic can be used to advantage on “mature” designs for which the anticipated result of the verification is pass.


  1. [BCM+92]
    J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang. Symbolic model checking: 1020 states and beyond. Information and Computation, 98(2):142–170, June 1992.Google Scholar
  2. [CES86]
    E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verifications of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244–263, April 1986.Google Scholar
  3. [Cle93]
    R. Cleaveland. A linear-time model-checking algorithm for the alternation-free modal μ-calculus. Formal Methods in System Design, 2:121–147, 1993.Google Scholar
  4. [CVWY91]
    C. Courcoubetis, M. Y. Vardi, P. Wolper, and M. Yannakakis. Memory efficient algorithms for the verification of temporal properties. Lecture Notes in Computer Science, 531:233–245, 1991.Google Scholar
  5. [EL86]
    E. A. Emerson and C. L. Lei. Efficient model checking in fragments of the propositional modal mu-calculus. In Proceedings of LICS 1986, pages 267–278, 1986.Google Scholar
  6. [HHK96]
    R. H. Hardin, Z. Har'El, and R. P. Kurshan. COSPAN. Lecture Notes in Computer Science, 1102:423–427, 1996.Google Scholar
  7. [HKM+96]
    R. H. Hardin, R. P. Kurshan, K. L. McMillan, J. A. Reeds, and N. J. A. Sloane. Efficient regression verification. IEE Proc. WODES'96, pages 147–150, 1996.Google Scholar
  8. [HTBK93]
    R. Hojati, H. J. Touati, R. K. Brayton, and R. P. Kurshan. Efficient ω-regular language containment. In Proceedings of CAV 93, LNCS 663, pages 396–409, 1993.Google Scholar
  9. [Kur94]
    R. P. Kurshan. Computer Aided Verification of Coordinating processes: An Automata Theoretic Approach. Princeton University Press, 1994.Google Scholar
  10. [LP85]
    O. Lichtenstein and A. Pnueli. Checking that finite state concurrent programs satisfy their linear specifications. In Conference Record of the Twelfth Annual ACM Symposium on Principles of Programming Languages, pages 97–107. ACM, ACM, January 1985.Google Scholar
  11. [McM93]
    K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.Google Scholar
  12. [TBK91]
    H. J. Touati, R. K. Brayton, and R. P. Kurshan. Testing language containment for omega-automata using BDD'S. In Proceedings of The 1991 International Workshop on Formal Methods in VLSI Design, January 1991.Google Scholar
  13. [TBK95]
    H. J. Touati, R. K. Brayton, and R. P. Kurshan. Testing language containment for ω-automata using BDD's. Information and Computation, 118(1):101–109, April 1995.Google Scholar
  14. [VW86]
    M.Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Proceedings of the First Symposium on Logic in Computer Science, pages 322–331, Cambridge, June 1986.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

  • R. H. Hardin
    • 1
  • R. P. Kurshan
    • 1
  • S. K. Shukla
    • 2
  • M. Y. Vardi
    • 3
  1. 1.Bell LabsMurray Hill
  2. 2.Computer Science DepartmentState University of New York at AlbanyNY
  3. 3.Department of Computer ScienceRice UniversityHouston

Personalised recommendations