Local Proofs for Global Safety Properties

This paper explores "local'' proofs for global safety properties of asynchronous, multi-process programs. Model checking on the full state space is often infeasible due to state explosion. A local proof, in contrast, is a collection of per-process invariants, which together imply the global safety property. The strongest local proof can be computed with a fixpoint procedure. Local proofs can be more compact; however, a central problem is that local reasoning is incomplete. In this paper, we present a ``completion'' algorithm, which gradually exposes facts about the internal state of components, until either a local proof or a real error is discovered. Experiments show that local reasoning can have significantly better performance over a reachability computation. Moreover, for some parameterized protocols, the generated local proof can be used to show correctness for all instances.