Affordable Access

Efficient Symbolic Model Checking of Software Using Partial Disjunctive Partitioning

IFIP Lecture Notes in Computer Science (LNCS)
Publication Date
  • Computer Science


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 , for which it is possible to generate small disjunctive partitions. By changing the image and pre-image procedures, we keep even smaller 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.Full Text at Springer, may require registration or fee

There are no comments yet on this publication. Be the first to share your thoughts.