Model Checking in Bits and Pieces

Fully automated verification of concurrent programs is a difficult problem, primarily because of state explosion: the exponential growth of a program state space with the number of its concurrently ac-tive components. It is natural to apply a divide and conquer strategy to ameliorate state explosion, by analyzing only a single component at a time. We show that this strategy leads to the notion of a “split ” invariant, an assertion which is globally inductive, while being structured as the conjunc-tion of a number of local, per-component invariants. This formulation is closely connected to the classical Owicki-Gries method and to Rely-Guarantee reasoning. We show how the division of an invariant into a number of pieces with limited scope makes it possible to apply new, localized forms of symmetry and abstraction to drastically simplify its computation. Split invariance also has inter-esting connections to parametric verification. A quantified invariant for a parametric system is a split invariant for every instance. We show how it is possible, in some cases, to invert this connection, and to automatically generalize from a split invariant for a small instance of a system to a quantified invariant which holds for the entire family of instances.