Advertisement

Interleaved Invariant Checking with Dynamic Abstraction

  • Liang Zhang
  • Mukul R. Prasad
  • Michael S. Hsiao
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3725)

Abstract

The notion of dynamic abstraction was recently introduced as a means of abstracting a model during the process of model checking. In this paper we show, theoretically and practically, how dynamic abstraction can be used with different algorithms for invariant checking, namely forward, backward and interleaved state-space traversal. Further, we formalize the correctness guarantees that can be made under different invariant checking algorithms operating on a dynamically abstracted model. We report experimental results on industrial strength benchmarks to further demonstrate the power and versatility of this abstraction mechanism in conjuction with interleaved state-space traversal.

Keywords

Model Check Abstract Model Model Check Algorithm Abstracted Model Empty Clause 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. 1.
    Amla, N., McMillan, K.L.: A hybrid of counterexample-based and proof-based abstraction. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol. 3312, pp. 260–274. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  2. 2.
    Bjesse, P., Kukula, J.: Using Counter Example Guided Abstraction Refinement to Find Complex Bugs. In: Proc. of the Design Automation and Test in Europe, February 2004, pp. 156–161 (2004)Google Scholar
  3. 3.
    Cabodi, G., Camurati, P., Quer, S.: Efficient State Space Pruning in Symbolic Backward Traversal. In: Proc. of the Intl. Conf. on Computer Design, October 1994, pp. 230–235 (1994)Google Scholar
  4. 4.
    Cabodi, G., Nocco, S., Quer, S.: Mixing Forward and Backward Traversals in Guided-Prioritized BDD-Based Verification. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, p. 471. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  5. 5.
    Chauhan, P., Clarke, E.M., Kukula, J., Sapra, S., Veith, H., Wang, D.: Automated Abstraction Refinement for Model Checking Large State Spaces using SAT based Conflict Analysis. In: Aagaard, M.D., O’Leary, J.W. (eds.) FMCAD 2002. LNCS, vol. 2517, pp. 33–51. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  6. 6.
    Clarke, E., Biere, A., Raimi, R., Zhu, Y.: Bounded Model Checking Using Satisfiability Solving. Formal Methods in System Design 19(1), 7–34 (2001)zbMATHCrossRefGoogle Scholar
  7. 7.
    Clarke, E.M., Gupta, A., Kukula, J., Strichman, O.: SAT-based Abstraction Refinement Using ILP and Machine Learning Techniques. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 265–279. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  8. 8.
    Glusman, M., Kamhi, G., Mador-Haim, S., Fraer, R., Vardi, M.Y.: Multiple-Counterexample Guided Iterative Abstraction Refinement: An Industrial Evaluation. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 176–191. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  9. 9.
    Goldberg, E., Novikov, Y.: Verification of proofs of unsatisfiability for CNF formulas. In: Proc. of the Design Automation and Test in Europe, March 2003, pp. 886–891 (2003)Google Scholar
  10. 10.
    Govindaraju, S.G., Dill, D.L.: Verification by approximate forward and backward reachability. In: Proc. of Intl. Conf. on CAD, November 1998, pp. 366–370 (1998)Google Scholar
  11. 11.
    Gupta, A., Ganai, M., Yang, Z., Ashar, P.: Iterative Abstraction Using SAT-based BMC with Proof Analysis. In: Proc. of the Intl. Conf. on CAD, November 2003, pp. 416–423 (2003)Google Scholar
  12. 12.
    Iwashita, H., Nakata, T.: Forward model checking techniques oriented to buggy designs. In: Proc. of Intl. Conf. on CAD, November 1997, pp. 400–404 (1997)Google Scholar
  13. 13.
    Kurshan, R.P.: Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach. Princeton University Press, Princeton (1995)zbMATHGoogle Scholar
  14. 14.
    Li, B., Somenzi, F.: Efficient Computation of Small Abstraction Refinements. In: Proc. of the Intl. Conf. on CAD (November 2004)Google Scholar
  15. 15.
    Mang, F.Y.-C., Ho, P.-H.: Abstraction Refinement by Controllability and Cooperativeness Analysis. In: Proc. of the Design Automation Conf., June 2004, pp. 224–229 (2004)Google Scholar
  16. 16.
    McMillan, K.L.: Symbolic Model Checking: An approach to the State Explosion Problem. Kluwer Academic Publishers, Dordrecht (1993)Google Scholar
  17. 17.
    McMillan, K.L., Amla, N.: Automatic abstraction without counterexamples. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 2–17. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  18. 18.
    Stangier, C., Sidle, T.: Invariant Checking Combining Forward and Backward Traversal. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol. 3312, pp. 414–429. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  19. 19.
    The VIS Group: VIS: A system for Verification and Synthesis. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 428–432. Springer, Heidelberg (1996)Google Scholar
  20. 20.
    VIS Verilog Benchmarks, http://vlsi.colorado.edu/~vis
  21. 21.
    Wang, C., Hachtel, G.D., Somenzi, F.: Fine-Grain Abstraction and Sequential Don’t Cares for Large Scale Model Checking. In: Proc. of the Intl. Conf. on Computer Design (October 2004)Google Scholar
  22. 22.
    Wang, C., Li, B., Jin, H., Hachtel, G.D., Somenzi, F.: Improving Ariadne’s Bundle by Following Multiple Threads in Abstraction Refinement. In: Proc. of the Intl. Conf. on CAD, November 2003, pp. 408–415 (2003)Google Scholar
  23. 23.
    Wang, D., Ho, P.-H., Long, J., Kukula, J., Zhu, Y., Ma, T., Damiano, R.: Formal Property Verification by Abstraction Refinement with Formal, Simulation and Hybrid Engines. In: Proc. of the Design Automation Conf., June 2001, pp. 35–40 (2001)Google Scholar
  24. 24.
  25. 25.
    Zhang, L., Malik, S.: Validating SAT Solvers using an Independent Resolution-based Checker: Practical Implementations and Other Applications. In: Proc. of the Design Automation and Test in Europe, March 2003, pp. 880–885 (2003)Google Scholar
  26. 26.
    Zhang, L., Prasad, M.R., Hsiao, M., Sidle, T.: Dynamic Abstraction Using SAT-based BMC. In: Proc. of the Design Automation Conf., June 2005, pp. 754–757 (2005)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Liang Zhang
    • 1
  • Mukul R. Prasad
    • 2
  • Michael S. Hsiao
    • 3
  1. 1.Cadence Design SystemsSan Jose
  2. 2.Fujitsu Laboratories of AmericaSunnyvale
  3. 3.Dept. of Electrical & Computer EngineeringVirginia Tech.Blacksburg

Personalised recommendations