Efficient Symbolic Model Checking of Software Using Partial Disjunctive Partitioning

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