model checking

Finite-state verification techniques are often hampered by the stateexplosion problem. One proposed approach for addressing this problem is assume-guarantee reasoning. We were interested in determining if assume-guarantee reasoning could provide an advantage over monolithic verification. Using recent advances in assume-guarantee reasoning that automatically generate assumptions, we undertook a study that considered all two-way decompositions for a set of systems and properties, using two different verifiers. By increasing the number of repeated tasks for a system, we evaluated the decompositions as the systems were scaled. In very few cases were we able to show that assume-guarantee reasoning could verify properties on larger systems than monolithic verification could. Additionally, assume-guarantee reasoning could only verify these properties on systems a few sizes larger than monolithic verification. This negative result, although preliminary, raises doubts about the usefulness of assume-guarantee reasoning as an effective technique