How Thorough Is Thorough Enough?
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.
- 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
- 6.Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)Google Scholar
- 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
- 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.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
- 20.Milner, R.: An Algebraic Definition of Simulation between Programs. In: AI 1971, pp. 481–489 (1971)Google Scholar