The Localization Reduction and Counterexample-Guided Abstraction Refinement | SpringerLink
Skip to main content
Springer Nature Link
Log in

The Localization Reduction and Counterexample-Guided Abstraction Refinement

  • Chapter
Time for Verification

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 6200))

Abstract

Automated abstraction is widely recognized as a key method for computer-aided verification of hardware and software. In this paper, we describe the evolution of counterexample-guided refinement and other iterative abstraction refinement techniques.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
JPY 3498
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
JPY 10295
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Alur, R., Itai, A., Kurshan, R.P., Yannakakis, M.: Timing Verification by Successive Approximation. In: Probst, D.K., von Bochmann, G. (eds.) CAV 1992. LNCS, vol. 663, pp. 137–150. Springer, Heidelberg (1993); Also Inf. Comput. 118(1), 142–157 (1995)

    Chapter  Google Scholar 

  2. 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)

    Chapter  Google Scholar 

  3. Amla, N., McMillan, K.L.: Combining Abstraction Refinement and SAT-Based Model Checking. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 405–419. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  4. Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without bdds. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  5. Ball, T., Rajamani, S.K.: The slam project: debugging system software via static analysis. In: POPL, pp. 1–3 (2002)

    Google Scholar 

  6. Chaki, S., Clarke, E.M., Groce, A., Jha, S., Veith, H.: Modular verification of software components in c. In: ICSE, pp. 385–395. IEEE Computer Society, Los Alamitos (2003)

    Google Scholar 

  7. Chauhan, P., Clarke, E.M., Kukula, J.H., 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)

    Chapter  Google Scholar 

  8. Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154–169. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  9. Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50(5), 752–794 (2003)

    Article  MathSciNet  MATH  Google Scholar 

  10. Clarke, E.M., Gupta, A., Kukula, J.H., 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)

    Chapter  Google Scholar 

  11. Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Trans. Program. Lang. Syst. 16(5), 1512–1542 (1994)

    Article  Google Scholar 

  12. Chaki, S.: A Counterexample Guided Abstraction Refinement Framework for Verifying Concurrent C Programs. PhD Thesis, Carnegie Mellon University (2005)

    Google Scholar 

  13. Clarke, E.M., Jha, S., Lu, Y., Veith, H.: Tree-like counterexamples in model checking. In: LICS, pp. 19–29. IEEE Computer Society Press, Los Alamitos (2002)

    Google Scholar 

  14. Clarke, E.M., Kroening, D., Sharygina, N., Yorav, K.: Satabs: Sat-based predicate abstraction for ansi-c. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 570–574. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  15. Cook, B., Podelski, A., Rybalchenko, A.: Abstraction refinement for termination. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol. 3672, pp. 87–101. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  16. Clarke, E.M., Veith, H.: Counterexamples revisited: Principles, algorithms, applications. In: Dershowitz, N. (ed.) Verification: Theory and Practice. LNCS, vol. 2772, pp. 208–224. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  17. Das, S., Dill, D.L.: Successive Approximation of Abstract Transition Relations. In: LICS 2001, pp. 51–58. IEEE Computer Society Press, Los Alamitos (2001)

    Google Scholar 

  18. Lucent’s Bell Introduces FormalCheck. Electronic News (April 1997)

    Google Scholar 

  19. Giacobazzi, R., Quintarelli, E.: Incompleteness, counterexamples, and refinements in abstract model-checking. In: Cousot, P. (ed.) SAS 2001. LNCS, vol. 2126, p. 356. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  20. Graf, S., Saıdi, H.: Construction of abstract state graphs with pvs. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  21. Hardin, R.H., Har’El, Z., Kurshan, R.P.: COSPAN. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 423–427. Springer, Heidelberg (1996)

    Chapter  Google Scholar 

  22. Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: POPL. ACM, New York (2004)

    Google Scholar 

  23. Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL, pp. 58–70 (2002)

    Google Scholar 

  24. Jhala, R., McMillan, K.L.: Interpolant-based transition relation approximation. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 39–51. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  25. Jhala, R., Majumdar, R.: Software model checking. ACM Comput. Surv. 41(4) (2009)

    Google Scholar 

  26. Kurshan, R.P.: Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach. Princeton University Press, Princeton (1994)

    MATH  Google Scholar 

  27. Kurshan, R.P.: Program Verification. Notices of the AMS 47(5), 534–545 (2000)

    MathSciNet  MATH  Google Scholar 

  28. Lu, Y.: Automated Abstraction in Model Checking. PhD Thesis, Carnegie Mellon University (2000)

    Google Scholar 

  29. 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)

    Chapter  Google Scholar 

  30. McMillan, K.L.: Interpolation and sat-based model checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 1–13. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  31. Pnueli, A.: Keynote address: Abstraction, composition, symmetry, and a little deduction: The remedies to state explosion. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, p. 1. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  32. Pnueli, A., Podelski, A., Rybalchenko, A.: Separating fairness and well-foundedness for the analysis of fair discrete systems. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 124–139. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  33. Podelski, A., Rybalchenko, A.: Transition invariants. In: LICS, pp. 32–41. IEEE Computer Society, Los Alamitos (2004)

    Google Scholar 

  34. Wagner, H.M.: Principles of Operations Research, pp. 953–958. Prentice Hall, Englewood Cliffs (1975); see Appendix I: Advanced Topics in Network Algorithms

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Computer Science, Carnegie Mellon University, Pittsburgh, PA

    Edmund M. Clarke

  2. Cadence Design Systems, Inc., New York, NY 10014

    Robert P. Kurshan

  3. Formal Methods in Systems Engineering, Vienna University of Technology, Austria

    Helmut Veith

Authors
  1. Edmund M. Clarke
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Robert P. Kurshan
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Helmut Veith
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Computer Science Department, Stanford University, 94305, Stanford, CA, USA

    Zohar Manna

  2. Department of Computer Science, Bar Ilan University, 52900, Ramat Gan, Israel

    Doron A. Peled

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Clarke, E.M., Kurshan, R.P., Veith, H. (2010). The Localization Reduction and Counterexample-Guided Abstraction Refinement. In: Manna, Z., Peled, D.A. (eds) Time for Verification. Lecture Notes in Computer Science, vol 6200. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-13754-9_4

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-13754-9_4

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-13753-2

  • Online ISBN: 978-3-642-13754-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation