Local Proofs for Global Safety Properties

This paper explores the concept of locality in proofs of global safety properties of asynchronously composed, 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. Local proofs can be compact: but 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, a local proof can be used to show correctness for all instances.

• Type: Conference
• Year: 2007
• Where: CAV
• Authors: Ariel Cohen 0002, Kedar S. Namjoshi
• Keywords: CAV 2007, Formal Methods, Global Safety, Local Proof, Local Reasoning