Efficient Symbolic Model Checking of Software Using Partial Disjunctive Partitioning

  • Sharon Barner
  • Ishai Rabinovitz
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2860)


This paper presents a method for taking advantage of the efficiency of symbolic model checking using disjunctive partitions, while keeping the number and the size of the partitions small. We define a restricted form of a Kripke structure, called an or-structure, for which it is possible to generate small disjunctive partitions. By changing the image and pre-image procedures, we keep even smaller partial disjunctive partitions in memory. In addition, we show how to translate a (software) program to an or-structure, in order to enable efficient symbolic model checking of the program using its disjunctive partitions. We build one disjunctive partition for each state variable in the model directly from the conjunctive partition of the same variable and independently of all other partitions. This method can be integrated easily into existing model checkers, without changing their input language, and while still taking advantage of reduction algorithms which prefer conjunctive partitions.


  1. 1.
    Beer, I., Ben-David, S., Eisner, C., Landver, A.: RuleBase: an industry-oriented formal verification tool. In: Proc. DAC 1996, pp. 655–660 (1996)Google Scholar
  2. 2.
    Cabodi, G., Camurati, P., Lavagno, L., Quer, S.: Disjunctive partitioning and partial iterative squaring: an effective approach for symbolic traversal of large circuits. In: Proc. DAC 1997, pp. 728–733 (1997)Google Scholar
  3. 3.
    Cabodi, G., Camurati, P., Quer, S.: Auxiliary variables for extending symbolic traversal techniques to data paths. In: Proc. DAC 1994, pp. 289–293 (1994)Google Scholar
  4. 4.
    Chan, W., Anderson, R., Beame, P., Notkin, D.: Improving efficiency of symbolic model checking for state-based system requirements. In: Proc. ISSTA 1998 (1998)Google Scholar
  5. 5.
    Eisner, C.: Model checking the garbage collection mechanism of SMV. In: Stoller, S.D., Visser, W. (eds.) Electronic Notes in Theoretical Computer, vol. 55, Elsevier Science Publishers, Amsterdam (2001)Google Scholar
  6. 6.
    Eisner, C., Peled, D.: Comparing symbolic and explicit model checking of a software system. In: Bošnački, D., Leue, S. (eds.) SPIN 2002. LNCS, vol. 2318, pp. 230–239. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  7. 7.
    Geist, D., Beer, I.: Efficient model checking by automated ordering of transition relation partitions. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 299–310. Springer, Heidelberg (1994)Google Scholar
  8. 8.
    Burch, J.R., Clarke, E.M., Long, D.E.: Symbolic model checking with partitioned transition relations. In: Halaas, A., Denyer, P.B. (eds.) International Conference on Very Large Scale Integration, pp. 49–58 (1991)Google Scholar
  9. 9.
    McMillan, K.: Symbolic Model Checking. Kluwer Academic Publishers, Dordrecht (1993)zbMATHGoogle Scholar
  10. 10.
    Solé, M., Pastor, E.: Traversal techniques for concurrent systems. In: Aagaard, M.D., O’Leary, J.W. (eds.) FMCAD 2002. LNCS, vol. 2517, pp. 220–237. Springer, Heidelberg (2002)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2003

Authors and Affiliations

  • Sharon Barner
    • 1
  • Ishai Rabinovitz
    • 1
  1. 1.IBM Haifa Research LaboratoryHaifaIsrael

Personalised recommendations