Advertisement

Better Under-Approximation of Programs by Hiding Variables

  • Thomas Ball
  • Orna Kupferman
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4349)

Abstract

Abstraction frameworks use under-approximating transitions in order to prove existential properties of concrete systems. Under-approximating transitions refer to the concrete states that correspond to a particular abstract state in a universal manner. For example, there is a must transition from abstract state a to abstract state a ′ only if all the concrete states in a have successors in a ′.

The universal nature of under-approximating transitions makes them closed under transitivity. Consequently, reachability queries about the concrete system, which have applications in falsification and testing, can be answered by reasoning about its abstraction. On the negative side, the universal nature of under-approximating transitions makes them dependent on all the variables of the program. The abstraction, on the other hand, often hides some of the variables. Since the universal quantification in must transitions ranges over all variables, this often prevents the abstraction from associating a must transition with statements that refer to hidden variables.

We introduce and study partitioned-must transitions. The idea is to partition the program variables to relevant and irrelevant ones, and restrict the universal quantification inside must transitions to the relevant variables. Usual must transitions are a special case of partitioned-must transitions in which all variables are relevant. Partitioned-must transitions exist in many realistic settings in which usual must transitions do not exist. As we show, they retain the advantages of must transitions: they are closed under transitivity, their calculation can be automated, and the three-valued semantics induced by usual must transitions is refined to a multi-valued semantics that takes into an account the set of relevant variables.

Keywords

Model Check Abstract State Safety Property Atomic Proposition Concrete State 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. FMCO 2004.
    Ball, T.: A theory of predicate-complete test coverage and generation. In: de Boer, F.S., et al. (eds.) FMCO 2004. LNCS, vol. 3657, Springer, Heidelberg (2005)CrossRefGoogle Scholar
  2. CONCUR 2000.
    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
  3. ICALP 2004.
    Bruns, G., Godefroid, P.: Model checking with 3-valued temporal logics. In: Díaz, J., et al. (eds.) ICALP 2004. LNCS, vol. 3142, pp. 281–293. Springer, Heidelberg (2004)Google Scholar
  4. IDEAL 2005.
    Ball, T., Kupferman, O., Yorsh, G.: Abstraction for falsification. In: Gallagher, M., Hogan, J.P., Maire, F. (eds.) IDEAL 2005. LNCS, vol. 3578, pp. 67–81. Springer, Heidelberg (2005)Google Scholar
  5. Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for the static analysis of programs by construction or approximation of fixpoints. In: Proc. 4th ACM POPL, pp. 238–252. ACM Press, New York (1977)Google Scholar
  6. Dijksta, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)Google Scholar
  7. CAV 2002.
    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
  8. ATVA 2006.
    Kupferman, O., Lampert, R.: On the construction of fine automata for safety properties. In: Graf, S., Zhang, W. (eds.) ATVA 2006. LNCS, vol. 4218, pp. 110–124. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  9. Kurshan, R.P.: Computer Aided Verification of Coordinating Processes. Princeton University Press, Princeton (1994)Google Scholar
  10. Larsen, K.G., Thomsen, G.B.: A modal process logic. In: Proc. 3th LICS (1988)Google Scholar
  11. Larsen, K.G., XinXin, L.: Equation solving using modal transition systems. In: Proc. 5th LICS, Philadelphia, pp. 108–117 (June 1990)Google Scholar
  12. CAV 2003.
    Shoham, S., Grumberg, O.: A game-based framework for CTL counterexamples and 3-valued abstraction-refinement. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 275–287. Springer, Heidelberg (2003)Google Scholar
  13. TACAS 2004.
    Shoham, S., Grumberg, O.: Monotonic abstraction-refinement for. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 546–560. Springer, Heidelberg (2004)Google Scholar
  14. Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. I. & C. 115(1), 1–37 (1994)zbMATHMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2007

Authors and Affiliations

  • Thomas Ball
    • 1
  • Orna Kupferman
    • 2
  1. 1.Microsoft Research, One Microsoft way, Redmond, WA, 98052USA
  2. 2.Hebrew University, School of Eng. and Comp. Sci., Jerusalem 91904Israel

Personalised recommendations