iBet uBet web content aggregator. Adding the entire web to your favor.
iBet uBet web content aggregator. Adding the entire web to your favor.



Link to original content: https://unpaywall.org/10.1007/978-3-319-10575-8_13
Abstraction and Abstraction Refinement | SpringerLink
Skip to main content
Springer Nature Link
Log in

Abstraction and Abstraction Refinement

  • Chapter
  • First Online:
Handbook of Model Checking

Abstract

Abstraction, in the context of model checking, is aimed at reducing the state space of the system by omitting details that are irrelevant to the property being verified. Many successful approaches to the “state explosion problem,” some of them described in other chapters, can be seen as abstractions. In this chapter, several notions of abstraction are considered in a uniform setting. Different such notions lead to a variety of preservation results that establish which kind of temporal properties may be verified via an abstracted system. We first define the needed background on simulation and bisimulation relations and their logic preservation. We then present the abstraction that is currently most widely used in practice: existential abstraction, which preserves universal fragments of branching-time logics. We give examples of such abstractions: localization reduction for hardware and predicate abstraction for software. We then proceed to stronger abstractions which preserve full branching-time logics. We introduce Kripke Modal Transition Systems and modal simulation, and show logic preservation. We close the chapter with a review of the presented results in the light of the notion of completeness.

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

Access this chapter

Log in via an institution

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. de Alfaro, L., Godefroid, P., Jagadeesan, R.: Three-valued abstractions of games: uncertainty, but with precision. In: Symp. on Logic in Computer Science (LICS), pp. 170–179. ACM, New York (2004)

    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.) Formal Methods in Computer Aided Design (FMCAD). LNCS, vol. 3312, pp. 260–274. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  3. Ball, T., Podelski, A., Rajamani, S.K.: Boolean and Cartesian abstraction for model checking C programs. In: Margaria, T., Yi, W. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 2031, pp. 268–283. Springer, Heidelberg (2001)

    Google Scholar 

  4. Ball, T., Rajamani, S.: Boolean programs: a model and process for software analysis. Tech. Rep. 2000-14, Microsoft Research (2000)

    Google Scholar 

  5. Ball, T., Rajamani, S.K.: The SLAM toolkit. In: Berry, G., Comon, H., Finkel, A. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 2102, pp. 260–264. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  6. Barner, S., Geist, D., Gringauze, A.: Symbolic localization reduction with reconstruction layering and backtracking. In: Intl. Conf. on Computer-Aided Verification (CAV). LNCS. Springer, Heidelberg (2002)

    Google Scholar 

  7. Beyer, D., Chlipala, A., Henzinger, T.A., Jhala, R., Majumdar, R.: The BLAST query language for software verification. In: Giacobazzi, R. (ed.) SAS. LNCS, vol. 3148, pp. 2–18. Springer, Heidelberg (2004)

    Google Scholar 

  8. Beyer, D., Henzinger, T.A., Théoduloz, G.: Configurable software verification: concretizing the convergence of model checking and program analysis. In: Damm, W., Hermanns, H. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 4590, pp. 504–518. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  9. Beyer, D., Henzinger, T.A., Théoduloz, G.: Program analysis with dynamic precision adjustment. In: Intl. Conf. on Automated Software Engineering (ASE), pp. 29–38. IEEE, Piscataway (2008)

    Google Scholar 

  10. Biere, A., Kroening, D.: SAT-based model checking. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018)

    Google Scholar 

  11. Bobaru, M.G., Pasareanu, C.S., Giannakopoulou, D.: Automated assume-guarantee reasoning by abstraction refinement. In: Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 5123, pp. 135–148. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  12. Bouajjani, A., Fernandez, J., Halbwachs, N.: Minimal model generation. In: Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 531, pp. 197–203. Springer, Heidelberg (1990)

    Chapter  Google Scholar 

  13. Bouali, A., de Simone, R.: Symbolic bisimulation minimisation. In: Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 663, pp. 96–108. Springer, Heidelberg (1992)

    Chapter  Google Scholar 

  14. Bradfield, J., Walukiewicz, I.: The mu-calculus and model checking. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018)

    Google Scholar 

  15. Browne, M.C., Clarke, E.M., Grumberg, O.: Characterizing finite Kripke structures in propositional temporal logic. Theor. Comput. Sci. 59(1–2), 115–131 (1988)

    Article  MathSciNet  Google Scholar 

  16. Bruns, G., Godefroid, P.: Model checking partial state spaces with 3-valued temporal logics. In: Intl. Conf. on Computer-Aided Verification (CAV). LNCS, pp. 274–287. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  17. Bruns, G., Godefroid, P.: Generalized model checking: reasoning about partial state spaces. In: Intl. Conf. on Concurrency Theory (CONCUR). LNCS, vol. 1877, pp. 168–182. Springer, Heidelberg (2000)

    Google Scholar 

  18. Bruns, G., Godefroid, P.: Model checking with multi-valued logics. In: Intl. Colloquium on Automata, Languages, and Programming (ICALP), pp. 281–293. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  19. Bryant, R.E., Beatty, D.L., Seger, C.J.H.: Formal hardware verification by symbolic ternary trajectory evaluation. In: Design Automation Conf. (DAC), pp. 397–402 (1991)

    Google Scholar 

  20. Bustan, D., Grumberg, O.: Simulation-based minimization. ACM Trans. Comput. Log. 4(2), 181–206 (2003)

    Article  MathSciNet  Google Scholar 

  21. Chaki, S., Gurfinkel, A.: BDD-based symbolic model checking. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018)

    MATH  Google Scholar 

  22. Chaki, S., Strichman, O.: Optimized L*-based assume-guarantee reasoning. In: Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, pp. 276–291. Springer, Heidelberg (2007)

    Google Scholar 

  23. Chauhan, P., Clarke, E., Kukula, J., Sapra, S., Veith, H., Wang, D.: Automated abstraction refinement for model checking large state spaces using SAT based conflict analysis. In: Formal Methods in Computer Aided Design (FMCAD). IEEE, Piscataway (2002)

    Google Scholar 

  24. Chechik, M., Devereux, B., Easterbrook, S., Gurfinkel, A.: Multi-valued symbolic model-checking. ACM Trans. Softw. Eng. Methodol. 12, 371–408 (2003)

    Article  Google Scholar 

  25. Chechik, M., Devereux, B., Gurfinkel, A., Easterbrook, S.: Multi-valued symbolic model-checking. Tech. Rep. CSRG-448, University of Toronto (2002)

    Google Scholar 

  26. Chen, Y., He, Y., Xie, F., Yang, J.: Automatic abstraction refinement for generalized symbolic trajectory evaluation. In: Formal Methods in Computer Aided Design (FMCAD). IEEE/ACM, Piscataway/New York (2007)

    Google Scholar 

  27. Chockler, H., Grumberg, O., Yadgar, A.: Efficient automatic STE refinement using responsibility. In: Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 4963. Springer, Heidelberg (2008)

    Google Scholar 

  28. Cimatti, A., Griggio, A., Micheli, A., Narasamdya, I., Roveri, M.: Kratos—a software model checker for SystemC. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV. LNCS, vol. 6806, pp. 310–316. Springer, Heidelberg (2011)

    Google Scholar 

  29. Cimatti, A., Narasamdya, I., Roveri, M.: Software model checking SystemC. IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst. 32(5), 774–787 (2013)

    Article  Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  31. Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)

    Google Scholar 

  32. Clarke, E., Gupta, A., Kukula, J., Strichman, O.: SAT based abstraction-refinement using ILP and machine learning techniques. In: Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 2404. Springer, Heidelberg (2002)

    Google Scholar 

  33. Clarke, E., Kroening, D., Sharygina, N., Yorav, K.: SATABS: SAT-Based Predicate Abstraction for ANSI-C. In: Halbwachs, N., Zuck, L.D. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 3440, pp. 570–574. Springer, Heidelberg (2005)

    MATH  Google Scholar 

  34. 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 

  35. Clarke, E.M., Jha, S., Lu, Y., Veith, H.: Tree-like counterexamples in model checking. In: Symp. on Logic in Computer Science (LICS), pp. 19–29. IEEE, Piscataway (2002)

    Google Scholar 

  36. Clarke, E.M., Kroening, D., Sharygina, N., Yorav, K.: Predicate abstraction of ANSI-C programs using SAT. Form. Methods Syst. Des. 25(2–3), 105–127 (2004)

    Article  Google Scholar 

  37. Cousot, P.: Abstract interpretation. ACM Comput. Surv. 28, 324–328 (1996)

    Article  Google Scholar 

  38. Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Symp. on Principles of Programming Languages (POPL), pp. 238–252. ACM, New York (1977)

    Google Scholar 

  39. Cousot, P., Cousot, R.: Temporal abstract interpretation. In: Symp. on Principles of Programming Languages (POPL), pp. 12–25. ACM, New York (2000)

    Google Scholar 

  40. Dams, D., Gerth, R., Grumberg, O.: Abstract interpretation of reactive systems. Trans. Program. Lang. Syst. 19(2), 253–291 (1997)

    Article  Google Scholar 

  41. Dams, D., Namjoshi, K.S.: The existence of finite abstractions for branching time model checking. In: Symp. on Logic in Computer Science (LICS), pp. 335–344. IEEE, Piscataway (2004)

    Google Scholar 

  42. Dams, D., Namjoshi, K.S.: Automata as abstractions. In: Intl. Conf. on Verification, Model Checking and Abstract Interpretation (VMCAI). LNCS, vol. 3385, pp. 216–232. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  43. De Nicola, R.: Extensional equivalences for transition systems. Acta Inform. 24(2), 211–237 (1987)

    Article  MathSciNet  Google Scholar 

  44. De Nicola, R., Vaandrager, F.W.: Three logics for branching bisimulation. J. ACM 42(2), 458–487 (1995)

    Article  MathSciNet  Google Scholar 

  45. Gazda, M., Willemse, T.A.C.: Expressiveness and completeness in abstraction. In: Luttik, B., Reniers, M.A. (eds.) Proc. Combined 19th Intl. Workshop on Expressiveness in Concurrency and 9th Workshop on Structured Operational Semantics, EXPRESS/SOS. EPTCS, vol. 89, pp. 49–64 (2012)

    Google Scholar 

  46. Godefroid, P., Jagadeesan, R.: Automatic abstraction using generalized model checking. In: Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 2404, pp. 137–150. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  47. Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  48. Grumberg, O.: Abstraction and refinement in model checking. In: Intl. Conf. on Formal Methods for Components and Objects (FMCO). LNCS, vol. 4111. Springer, Heidelberg (2005)

    Google Scholar 

  49. Grumberg, O., Lange, M., Leucker, M., Shoham, S.: Don’t know in \(\mu\)-calculus. In: Intl. Conf. on Verification, Model Checking and Abstract Interpretation (VMCAI). LNCS. Springer, Heidelberg (2005)

    Google Scholar 

  50. Grumberg, O., Lange, M., Leucker, M., Shoham, S.: When not losing is better than winning: abstraction and refinement for the full mu-calculus. Inf. Comput. 205, 1130–1148 (2007)

    Article  Google Scholar 

  51. Grumberg, O., Long, D.E.: Model checking and modular verification. ACM Trans. Program. Lang. Syst. 16, 843–872 (1994)

    Article  Google Scholar 

  52. Grumberg, O., Schuster, A., Yadgar, A.: 3-valued circuit SAT for STE with automatic refinement. In: Intl. Symp. Automated Technology for Verification and Analysis (ATVA). LNCS, vol. 4762. Springer, Heidelberg (2007)

    Google Scholar 

  53. Gupta, A., Ganai, M., Yang, Z., Ashar, P.: Iterative abstraction using SAT-based BMC with proof analysis. In: International Conference on Computer Aided Design (ICCAD), p. 416. IEEE, Piscataway (2003)

    Google Scholar 

  54. Gupta, A., Strichman, O.: Abstraction refinement for bounded model checking. In: Etessami, K., Rajamani, S. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 3576, pp. 112–124. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  55. Gurfinkel, A., Chechik, M.: Why waste a perfectly good abstraction? In: Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, pp. 212–226. Springer, Heidelberg (2006)

    Google Scholar 

  56. Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. J. ACM 32(1), 137–161 (1985)

    Article  MathSciNet  Google Scholar 

  57. Henzinger, M.R., Henzinger, T.A., Kopke, P.W.: Computing simulations on finite and infinite graphs. In: FOCS: Foundations of Computer Science, pp. 453–462. IEEE, Piscataway (1995)

    Google Scholar 

  58. Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: Symp. on Principles of Programming Languages (POPL), pp. 232–244. ACM, New York (2004)

    Google Scholar 

  59. Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: Jones, N.D., Leroy, X. (eds.) POPL, pp. 232–244. ACM, New York (2004)

    Google Scholar 

  60. Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pp. 58–70. ACM, New York (2002)

    Chapter  Google Scholar 

  61. Huth, M., Jagadeesan, R., Schmidt, D.: Modal transition systems: a foundation for three-valued program analysis. In: Sands, D. (ed.) Programming Languages and Systems. LNCS, vol. 2028, pp. 155–169. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  62. Jain, H., Ivancic, F., Gupta, A., Shlyakhter, I., Wang, C.: Using statically computed invariants inside the predicate abstraction and refinement loop. In: Ball, T., Jones, R.B. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 4144, pp. 137–151. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  63. Jain, H., Kroening, D., Sharygina, N., Clarke, E.: Word level predicate abstraction and refinement for verifying RTL Verilog. IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst. 27, 366–379 (2008)

    Article  Google Scholar 

  64. Jhala, R., McMillan, K.: Array abstractions from proofs. In: Damm, W., Hermanns, H. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 4590, pp. 193–206. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  65. Jhala, R., Podelski, A., Rybalchenko, A.: Predicate abstraction for program verification. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018)

    Google Scholar 

  66. Kesten, Y., Pnueli, A.: Verification by augmented finitary abstraction. Inf. Comput. 163(1), 203–243 (2000)

    Article  MathSciNet  Google Scholar 

  67. Kozen, D.: Results on the propositional \(\mu\)-calculus. In: 9th Colloquium on Automata, Languages and Programming (ICALP). LNCS, vol. 140, pp. 348–359. Springer, Heidelberg (1982)

    Chapter  Google Scholar 

  68. Kroening, D., Sharygina, N.: Image computation and predicate refinement for RTL Verilog using word level proofs. In: Lauwereins, R., Madsen, J. (eds.) Design, Automation & Test in Europe (DATE), pp. 1325–1330. ACM, New York (2007)

    Google Scholar 

  69. Kroening, D., Weissenbacher, G.: Interpolation-based software verification with Wolverine. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV. LNCS, vol. 6806, pp. 573–578. Springer, Heidelberg (2011)

    Google Scholar 

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

    MATH  Google Scholar 

  71. Lahiri, S.K., Ball, T., Cook, B.: Predicate abstraction via symbolic decision procedures. Log. Methods Comput. Sci. 3(2) (2007)

    Google Scholar 

  72. Larsen, K., Thomsen, B.: A modal process logic. In: Symp. on Logic in Computer Science (LICS), pp. 203–210. IEEE, Piscataway (1988)

    Google Scholar 

  73. Larsen, K.G., Xinxin, L.: Equation solving using modal transition systems. In: Symp. on Logic in Computer Science (LICS), pp. 108–117. IEEE, Piscataway (1990)

    Google Scholar 

  74. Lee, D., Yannakakis, M.: Online minimization of transition systems (extended abstract). In: Proceedings of the 24th Annual ACM Symposium on Theory of Computing, pp. 264–274. ACM, New York (1992)

    Google Scholar 

  75. Li, B., Wang, C., Somenzi, F.: Abstraction refinement in symbolic model checking using satisfiability as the only decision procedure. Int. J. Softw. Tools Technol. Transf. 7(2), 143–155 (2005)

    Article  Google Scholar 

  76. Loiseaux, C., Graf, S., Sifakis, J., Bouajjani, A., Bensalem, S.: Property preserving abstractions for the verification of concurrent systems. Form. Methods Syst. Des. 6, 11–45 (1995)

    Article  Google Scholar 

  77. Mandrykin, M., Mutilin, V., Novikov, E., Khoroshilov, A.V., Shved, P.: Using Linux device drivers for static verification tools benchmarking. Program. Comput. Softw. 38(5), 245–256 (2012)

    Article  Google Scholar 

  78. McMillan, K.L.: Lazy abstraction with interpolants. In: Ball, T., Jones, R.B. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 4144, pp. 123–136. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  79. McMillan, K.L., Amla, N.: Automatic abstraction without counterexamples. In: Garavel, H., Hatcliff, J. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 2619, pp. 2–17. Springer, Heidelberg (2003)

    Google Scholar 

  80. Meller, Y., Grumberg, O., Shoham, S.: A framework for compositional verification of multi-valued systems via abstraction-refinement. In: Liu, Z., Ravn, A.P. (eds.) Intl. Symp. Automated Technology for Verification and Analysis (ATVA). LNCS, vol. 5799, pp. 271–288. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  81. Milner, R.: An algebraic definition of simulation between programs. In: Intl. Joint Conf. on Artificial Intelligence (IJCAI), pp. 481–489. British Computer Society, London (1971)

    Google Scholar 

  82. Namjoshi, K.: Abstraction for branching time properties. In: Hunt, W.A., Somenzi, F. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 2725, pp. 288–300. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  83. Park, D.: Concurrency and automata on infinite sequences. In: 5th GI-Conference on Theoretical Computer Science. LNCS, vol. 104, pp. 167–183. Springer, Heidelberg (1981)

    Chapter  Google Scholar 

  84. Piterman, N., Pnueli, A.: Temporal logic and fair discrete systems. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018)

    Google Scholar 

  85. Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. In: Symp. on Principles of Programming Languages (POPL), pp. 105–118. ACM, New York (1999)

    Google Scholar 

  86. Saïdi, H.: Model checking guided abstraction and analysis. In: Palsberg, J. (ed.) Intl. Symp. on Static Analysis (SAS). LNCS, vol. 1824, pp. 377–396. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  87. Saïdi, H., Shankar, N.: Abstract and model check while you prove. In: Halbwachs, N., Peled, D. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 1633, pp. 443–454. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  88. Seshia, S.A., Sharygina, N., Tripakis, S.: Modeling for verification. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018)

    Google Scholar 

  89. Sharygina, N., Tonetta, S., Tsitovich, A.: An abstraction refinement approach combining precise and approximated techniques. Int. J. Softw. Tools Technol. Transf. 14(1), 1–14 (2012)

    Article  Google Scholar 

  90. Shoham, S., Grumberg, O.: Monotonic abstraction-refinement for CTL. In: Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 2988, pp. 331–346 (2004)

    Google Scholar 

  91. Shoham, S., Grumberg, O.: Multi-valued model checking games. In: Peled, D.A., Tsay, Y.K. (eds.) Intl. Symp. Automated Technology for Verification and Analysis (ATVA). LNCS, vol. 3707, pp. 354–369. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  92. Shoham, S., Grumberg, O.: Compositional verification and 3-valued abstractions join forces. In: SAS’07. LNCS, vol. 4634. Springer, Heidelberg (2007)

    Google Scholar 

  93. Shoham, S., Grumberg, O.: A game-based framework for CTL counterexamples and 3-valued abstraction-refinement. ACM Transactions on Computer Logic (TOCL) 9 (2007)

    Article  MathSciNet  Google Scholar 

  94. Shoham, S., Grumberg, O.: 3-valued abstraction: more precision at less cost. Inf. Comput. 206(11), 1313–1333 (2008)

    Article  MathSciNet  Google Scholar 

  95. Singh, R., Giannakopoulou, D., Pasareanu, C.: Learning component interfaces with may and must abstractions. In: Touili, T., Cook, B., Jackson, P. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 6174, pp. 527–542. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  96. Stirling, C.: Modal and Temporal Properties of Processes. Texts in Computer Science. Springer, Heidelberg (2001)

    Book  Google Scholar 

  97. Tzoref, R., Grumberg, O.: Automatic refinement and vacuity detection for symbolic trajectory evaluation. In: Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 4144, pp. 190–204 (2006)

    Chapter  Google Scholar 

  98. Uribe, T.: Abstraction-based deductive-algorithmic verification of reactive systems. Ph.D. thesis, Computer Science Department, Stanford University (1998). Technical report STAN-CS-TR-99-1618

    Google Scholar 

  99. Vizel, Y., Grumberg, O., Shoham, S.: Lazy abstraction and SAT-based reachability in hardware model checking. In: Formal Methods in Computer Aided Design (FMCAD), pp. 173–181. IEEE, Piscataway (2012)

    Google Scholar 

  100. Wachter, B., Kroening, D., Ouaknine, J.: Verifying multi-threaded software with impact. In: Formal Methods in Computer Aided Design (FMCAD), pp. 210–217. IEEE, Piscataway (2013)

    Google Scholar 

  101. Wikipedia: The free encyclopedia. www.wikipedia.org (2011). Accessed 15 Nov. 2015

  102. Witkowski, T., Blanc, N., Kroening, D., Weissenbacher, G.: Model checking concurrent Linux device drivers. In: Intl. Conf. on Automated Software Engineering (ASE), ASE ’07, pp. 501–504. ACM, New York (2007)

    Google Scholar 

  103. Yahav, E., Reps, T., Sagiv, M.: LTL model checking for systems with unbounded number of dynamically created threads and objects. Tech. Rep. TR-1424, Computer Sciences Department, University of Wisconsin, Madison, WI (2001)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Embedded Systems Innovation by TNO, Eindhoven, The Netherlands

    Dennis Dams

  2. Technion, Israel Institute of Technology, Technion City, Haifa, Israel

    Orna Grumberg

Authors
  1. Dennis Dams
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Orna Grumberg
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Orna Grumberg .

Editor information

Editors and Affiliations

  1. FORE Systems University Professor of Computer Science, Carnegie Mellon University, Pittsburgh, Pennsylvania, USA

    Edmund M. Clarke

  2. Institute of Science and Technology Austria (IST), Klosterneuburg, Austria

    Thomas A. Henzinger

  3. Arbeitsbereich Formal Methods in Systems Engineering, Technische Universität Wien, Wien, Austria

    Helmut Veith

  4. Institut f. Angewandte Informationsverarbeitung und Kommunikationstechnologie (IAIK), Technische Universität Graz, Graz, Austria

    Roderick Bloem

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG, part of Springer Nature

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Dams, D., Grumberg, O. (2018). Abstraction and Abstraction Refinement. In: Clarke, E., Henzinger, T., Veith, H., Bloem, R. (eds) Handbook of Model Checking. Springer, Cham. https://doi.org/10.1007/978-3-319-10575-8_13

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-10575-8_13

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-10574-1

  • Online ISBN: 978-3-319-10575-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation