Efficient symbolic model checking of software using partial disjunctive partitioning

Abstract

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. © Springer-Verlag Berlin Heidelberg 2003.