How Thorough Is Thorough Enough?

  • Arie Gurfinkel
  • Marsha Chechik
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3725)


Abstraction is the key for effectively dealing with the state explosion problem in model-checking. Unfortunately, finding abstractions which are small and yet enable us to get conclusive answers about properties of interest is notoriously hard. Counterexample-guided abstraction refinement frameworks have been proposed to help build good abstractions iteratively. Although effective in many cases, such frameworks can include unnecessary refinement steps, leading to larger models, because the abstract verification step is not as conclusive as it can be in theory. Abstract verification can be supplemented by a more precise but much more expensive thorough check, but it is not clear how often this check really helps. In this paper, we study the relationship between model-checking and thorough checking and identify practical cases where the latter is not necessary, and those where it can be performed efficiently.


  1. 1.
    Ball, T., Podelski, A., Rajamani, S.: Boolean and Cartesian Abstraction for Model Checking C Programs. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 268–283. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  2. 2.
    Bruns, G., Godefroid, P.: Model Checking Partial State Spaces with 3-Valued Temporal Logics. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 274–287. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  3. 3.
    Bruns, G., Godefroid, P.: Generalized Model Checking: Reasoning About Partial State Spaces. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 168–182. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  4. 4.
    Chechik, M., Devereux, B., Easterbrook, S., Gurfinkel, A.: Multi-Valued Symbolic Model-Checking. ACM Trans. on Soft. Eng. and Methodology 12(4), 1–38 (2003)Google Scholar
  5. 5.
    Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-Guided Abstraction Refinement for Symbolic Model Checking. Journal of the ACM 50(5), 752–794 (2003)CrossRefMathSciNetGoogle Scholar
  6. 6.
    Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)Google Scholar
  7. 7.
    Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications. ACM Trans. on Prog. Lang. and Systems 8(2), 244–263 (1986)zbMATHCrossRefGoogle Scholar
  8. 8.
    Cousot, P., Cousot, R.: Abstract Interpretation: A Unified Lattice Model For Static Analysis of Programs by Construction or Approximation of Fixpoints. In: Proceedings of the 4th POPL, Los Angeles, California, pp. 238–252 (1977)Google Scholar
  9. 9.
    Dams, D., Gerth, R., Grumberg, O.: Abstract Interpretation of Reactive Systems. ACM Trans. on Prog. Lang. and Systems 2(19), 253–291 (1997)CrossRefGoogle Scholar
  10. 10.
    French, T.: Decidability of Quantifed Propositional Branching Time Logics. In: Stumptner, M., Corbett, D.R., Brooks, M. (eds.) Canadian AI 2001. LNCS (LNAI), vol. 2256, pp. 165–176. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  11. 11.
    Godefroid, P., Huth, M., Jagadeesan, R.: Abstraction-Based Model Checking Using Modal Transition Systems. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 426–440. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  12. 12.
    Godefroid, P., Jagadeesan, R.: Automatic Abstraction Using Generalized Model-Checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 137–150. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  13. 13.
    Godefroid, P., Jagadeesan, R.: On the Expressiveness of 3-Valued Models. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds.) VMCAI 2003. LNCS, vol. 2575, pp. 206–222. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  14. 14.
    Graf, S., Saïdi, H.: Construction of Abstract State Graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254. Springer, Heidelberg (1997)Google Scholar
  15. 15.
    Gurfinkel, A., Chechik, M.: Generating Counterexamples for Multi-Valued Model-Checking. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805. Springer, Heidelberg (2003)Google Scholar
  16. 16.
    Gurfinkel, A., Chechik, M.: Multi-Valued Model-Checking via Classical Model-Checking. In: Amadio, R.M., Lugiez, D. (eds.) CONCUR 2003. LNCS, vol. 2761, pp. 266–280. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  17. 17.
    Gurfinkel, A., Chechik, M.: Extending Extended Vacuity. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol. 3312, pp. 306–321. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  18. 18.
    Kleene, S.C.: Introduction to Metamathematics. Van Nostrand, New York (1952)zbMATHGoogle Scholar
  19. 19.
    Kupferman, O.: Augmenting Branching Temporal Logics with Existential Quantification over Atomic Propositions. J. of Logic and Computation 7, 1–14 (1997)CrossRefGoogle Scholar
  20. 20.
    Milner, R.: An Algebraic Definition of Simulation between Programs. In: AI 1971, pp. 481–489 (1971)Google Scholar
  21. 21.
    Müller-Olm, M., Schmidt, D., Steffen, B.: Model-Checking: A Tutorial Introduction. In: Cortesi, A., Filé, G. (eds.) SAS 1999. LNCS, vol. 1694, pp. 330–354. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  22. 22.
    Shoham, S., Grumberg, O.: A Game-Based Framework for CTL Counter-Examples and 3-Valued Abstraction-Refinement. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 275–287. Springer, Heidelberg (2003)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Arie Gurfinkel
    • 1
  • Marsha Chechik
    • 1
  1. 1.Department of Computer ScienceUniversity of Toronto 

Personalised recommendations